1  /-
  2  Copyright (c) 2018 Patrick Massot. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Normed spaces.
  5  
  6  Authors: Patrick Massot, Johannes Hölzl
  7  -/
  8  
  9  import algebra.pi_instances
src         └──────────────────┘
 10  import linear_algebra.basic
src         └──────────────────┘
 11  import topology.instances.nnreal topology.instances.complex
src         └───────────────────────┘ └────────────────────────┘
 12  import topology.algebra.module
src         └─────────────────────┘
 13  
 14  variables {α : Type*} {β : Type*} {γ : Type*} {ι : Type*}
 15  
 16  noncomputable theory
 17  open filter metric
 18  open_locale topological_space
 19  localized "notation f `→_{`:50 a `}`:0 b := filter.tendsto f (_root_.nhds a) (_root_.nhds b)" in filter
 20  
 21  /-- Auxiliary class, endowing a type `α` with a function `norm : α → ℝ`. This class is designed to
 22  be extended in more interesting classes specifying the properties of the norm. -/
 23  class has_norm (α : Type*) := (norm : α → ℝ)
id                       └───┘               
src                                            
typ                      └───┘               
 24  
 25  export has_norm (norm)
 26  
 27  notation `∥`:1024 e:1 `∥`:1 := norm e
id                                  └──┘
src                                 └──┘
typ                                 └──┘
 28  
 29  section prio
 30  set_option default_priority 100 -- see Note [default priority]
doc             └──────────────┘
 31  /-- A normed group is an additive group endowed with a norm for which `dist x y = ∥x - y∥` defines
 32  a metric space structure. -/
 33  class normed_group (α : Type*) extends has_norm α, add_comm_group α, metric_space α :=
id                           └───┘          └──────┘   └────────────┘   └──────────┘ 
src                                         └──────┘    └────────────┘    └──────────┘
typ                          └───┘          └──────┘   └────────────┘   └──────────┘ 
doc                                         └──────┘                      └──────────┘
 34  (dist_eq : ∀ x y, dist x y = norm (x - y))
id                   └──┘    └──┘    
src                                      
typ                  └──┘    └──┘    
 35  end prio
 36  
 37  /-- Construct a normed group from a translation invariant distance -/
 38  def normed_group.of_add_dist [has_norm α] [add_comm_group α] [metric_space α]
 39    (H1 : ∀ x:α, ∥x∥ = dist x 0)
 40    (H2 : ∀ x y z : α, dist x y ≤ dist (x + z) (y + z)) : normed_group α :=
id                                                                     └┘ 
src                                                                    └┘
typ                                                                    └┘ 
doc                                                                    └┘
 41  { dist_eq := λ x y, begin
id                   
typ                  
st                       └─────
 42      rw H1, apply le_antisymm,
id          └┘        └─────────┘
src      └─┘    └────┘└─────────┘
typ      └─┘└┘  └────┘└─────────┘
doc      └─┘    └────┘
txt      └─┘    └────┘
par      └─┘    └────┘
pid                 
st   ────────┘└─────────────────┘└─
 43      { rw [sub_eq_add_neg, ← add_right_neg y], apply H2 },
id             └────────────┘    └───────────┘ 
src        └──┘└────────────┘└──┘└───────────┘   └────┘  
typ        └──┘└────────────┘└──┘└───────────┘  └────┘  
doc        └──┘              └──┘                └────┘  
txt        └──┘              └──┘                └────┘  
par        └──┘              └──┘                └────┘  
pid          └┘              └──┘                       
st   ─────┘└────────────────┘└─────────────────┘└──────────┘└┘
 44      { have := H2 (x-y) 0 y, rwa [sub_add_cancel, zero_add] at this }
id                 └┘              └────────────┘  └──────┘
src        └──────┘     └──┘   └───┘└────────────┘└┘└──────┘└────────┘
typ        └──────┘└┘  └──┘  └───┘└────────────┘└┘└──────┘└────────┘
doc        └──────┘      └──┘   └───┘              └┘        └────────┘
txt        └──────┘      └──┘   └───┘              └┘        └────────┘
par        └──────┘      └──┘   └───┘              └┘        └────────┘
pid        └───┘└─┘      └──┘      └┘              └┘        └──────┘
st   ─────────────────────────┘└───────────────────┘└────────┘└───────┘└─
 45    end }
st   ────┘
 46  
 47  /-- Construct a normed group from a translation invariant distance -/
 48  def normed_group.of_add_dist' [has_norm α] [add_comm_group α] [metric_space α]
id                                  └──────┘    └────────────┘    └──────────┘ 
src                                 └──────┘     └────────────┘     └──────────┘
typ                                 └──────┘    └────────────┘    └──────────┘ 
doc                                 └──────┘                        └──────────┘
 49    (H1 : ∀ x:α, ∥x∥ = dist x 0)
id                   └──┘ 
src                    └──┘
typ                  └──┘ 
 50    (H2 : ∀ x y z : α, dist (x + z) (y + z) ≤ dist x y) : normed_group α :=
id                       └──┘            └──┘      └──────────┘ 
src                       └──┘                └──┘        └──────────┘
typ                      └──┘            └──┘      └──────────┘ 
doc                                                          └──────────┘
 51  { dist_eq := λ x y, begin
id                   
typ                  
st                       └─────
 52      rw H1, apply le_antisymm,
id          └┘        └─────────┘
src      └─┘    └────┘└─────────┘
typ      └─┘└┘  └────┘└─────────┘
doc      └─┘    └────┘
txt      └─┘    └────┘
par      └─┘    └────┘
pid                 
st   ────────┘└─────────────────┘└─
 53      { have := H2 (x-y) 0 y, rwa [sub_add_cancel, zero_add] at this },
id                 └┘              └────────────┘  └──────┘
src        └──────┘     └──┘   └───┘└────────────┘└┘└──────┘└────────┘
typ        └──────┘└┘  └──┘  └───┘└────────────┘└┘└──────┘└────────┘
doc        └──────┘      └──┘   └───┘              └┘        └────────┘
txt        └──────┘      └──┘   └───┘              └┘        └────────┘
par        └──────┘      └──┘   └───┘              └┘        └────────┘
pid        └───┘└─┘      └──┘      └┘              └┘        └──────┘
st   ─────┘└──────────────────┘└───────────────────┘└────────┘└───────┘└┘
 54      { rw [sub_eq_add_neg, ← add_right_neg y], apply H2 }
id             └────────────┘    └───────────┘ 
src        └──┘└────────────┘└──┘└───────────┘   └────┘  
typ        └──┘└────────────┘└──┘└───────────┘  └────┘  
doc        └──┘              └──┘                └────┘  
txt        └──┘              └──┘                └────┘  
par        └──┘              └──┘                └────┘  
pid          └┘              └──┘                       
st   ───────────────────────┘└─────────────────┘└──────────┘└─
 55    end }
st   ────┘
 56  
 57  /-- A normed group can be built from a norm that satisfies algebraic properties. This is
 58  formalised in this structure. -/
 59  structure normed_group.core (α : Type*) [add_comm_group α] [has_norm α] : Prop :=
id                                    └───┘   └────────────┘    └──────┘ 
src                                           └────────────┘     └──────┘
typ                                   └───┘   └────────────┘    └──────┘ 
doc                                                              └──────┘
 60  (norm_eq_zero_iff : ∀ x : α, ∥x∥ = 0 ↔ x = 0)
id                                    
src                                       
typ                                   
 61  (triangle : ∀ x y : α, ∥x + y∥ ≤ ∥x∥ + ∥y∥)
id                              
src                                   
typ                             
 62  (norm_neg : ∀ x : α, ∥-x∥ = ∥x∥)
id                        
src                           
typ                       
 63  
 64  /-- Constructing a normed group from core properties of a norm, i.e., registering the distance and
 65  the metric space structure from the norm properties. -/
 66  noncomputable def normed_group.of_core (α : Type*) [add_comm_group α] [has_norm α]
id                                                       └────────────┘    └──────┘ 
src                                                      └────────────┘     └──────┘
typ                                                      └────────────┘    └──────┘ 
doc                                                                         └──────┘
 67    (C : normed_group.core α) : normed_group α :=
id          └───────────────┘     └──────────┘ 
src         └───────────────┘      └──────────┘
typ         └───────────────┘     └──────────┘ 
doc         └───────────────┘      └──────────┘
 68  { dist := λ x y, ∥x - y∥,
id                   
src                      
typ                  
 69    dist_eq := assume x y, by refl,
id                        
src                              └──┘
typ                            └──┘
doc                              └──┘
txt                              └──┘
par                              └──┘
st                              └───┘
 70    dist_self := assume x, (C.norm_eq_zero_iff (x - x)).mpr (show x - x = 0, by simp),
id                            └───────────────┘      └─┘           
src                             └───────────────┘        └─┘                    └──┘
typ                           └───────────────┘      └─┘                  └──┘
doc                                                                                └──┘
txt                                                                                └──┘
par                                                                                └──┘
st                                                                                └───┘
 71    eq_of_dist_eq_zero := assume x y h, show (x = y), from sub_eq_zero.mp $ (C.norm_eq_zero_iff (x - y)).mp h,
id                                                      └─────────┘└─┘    └───────────────┘      └┘  
src                                                          └─────────┘└─┘     └───────────────┘        └┘
typ                                                     └─────────┘└─┘    └───────────────┘      └┘  
 72    dist_triangle := assume x y z,
id                               
typ                              
 73      calc ∥x - z∥ = ∥x - y + (y - z)∥ : by simp
id                         
src                                    └────
typ                              └────
doc                                            └────
txt                                            └────
par                                            └────
pid                                                
st                                            └─────
 74              ... ≤ ∥x - y∥ + ∥y - z∥  : C.triangle _ _,
id                               └───────┘
src  ───────────┘                     └───────┘
typ  ───────────┘                └───────┘
doc  ───────────┘
txt  ───────────┘
par  ───────────┘
pid  ───────────┘
st   ───────────┘
 75    dist_comm := assume x y,
id                          
typ                         
 76      calc ∥x - y∥ = ∥ -(y - x)∥ : by simp
id                      
src                               └────
typ                           └────
doc                                      └────
txt                                      └────
par                                      └────
pid                                          
st                                      └─────
 77               ... = ∥y - x∥ : by { rw [C.norm_neg] } }
id                        
src  ────────────┘                  └──┘          └┘
typ  ────────────┘                └──┘└────────┘└┘
doc  ────────────┘                     └──┘          └┘
txt  ────────────┘                     └──┘          └┘
par  ────────────┘                     └──┘          └┘
pid  ────────────┘                       └┘          
st   ────────────┘                  └───────────────┘└┘
 78  
 79  section normed_group
 80  variables [normed_group α] [normed_group β]
id              └──────────┘     └──────────┘
src             └──────────┘     └──────────┘
typ             └──────────┘     └──────────┘
doc             └──────────┘     └──────────┘
 81  
 82  lemma dist_eq_norm (g h : α) : dist g h = ∥g - h∥ :=
id                                 └──┘      
src                                 └──┘          
typ                                └──┘      
 83  normed_group.dist_eq _ _
id   └──────────────────┘
src  └──────────────────┘
typ  └──────────────────┘
 84  
 85  @[simp] lemma dist_zero_right (g : α) : dist g 0 = ∥g∥ :=
id                                          └──┘     
src                                          └──┘       
typ                                         └──┘     
doc    └──┘
 86  by rw [dist_eq_norm, sub_zero]
id          └──────────┘  └──────┘
src     └──┘└──────────┘└┘└──────┘└─
typ     └──┘└──────────┘└┘└──────┘└─
doc     └──┘            └┘        └─
txt     └──┘            └┘        └─
par     └──┘            └┘        └─
pid       └┘            └┘        
st     └───────────────┘└────────┘
 87  
src  
typ  
doc  
txt  
par  
pid  
st   
 88  lemma norm_sub_rev (g h : α) : ∥g - h∥ = ∥h - g∥ :=
id                                       
src                                           
typ                                      
 89  by simpa only [dist_eq_norm] using dist_comm g h
id                  └──────────┘        └───────┘  
src     └──────────┘└──────────┘└──────┘└───────┘  
typ     └──────────┘└──────────┘└──────┘└───────┘
doc     └──────────┘            └──────┘           
txt     └──────────┘            └──────┘           
par     └──────────┘            └──────┘           
pid          └──┘└┘            └────┘           
st     └──────────────────────────────────────────────
 90  
src  
typ  
doc  
txt  
par  
pid  
st   
 91  @[simp] lemma norm_neg (g : α) : ∥-g∥ = ∥g∥ :=
id                                     
src                                       
typ                                    
doc    └──┘
 92  by simpa using norm_sub_rev 0 g
id                  └──────────┘   
src     └──────────┘└──────────┘└─┘ 
typ     └──────────┘└──────────┘└─┘
doc     └──────────┘            └─┘ 
txt     └──────────┘            └─┘ 
par     └──────────┘            └─┘ 
pid          └────┘            └─┘ 
st     └─────────────────────────────
 93  
src  
typ  
doc  
txt  
par  
pid  
st   
 94  @[simp] lemma dist_add_left (g h₁ h₂ : α) : dist (g + h₁) (g + h₂) = dist h₁ h₂ :=
id                                              └──┘    └┘     └┘   └──┘ └┘ └┘
src                                              └──┘                  └──┘
typ                                             └──┘    └┘     └┘   └──┘ └┘ └┘
doc    └──┘
 95  by simp [dist_eq_norm]
id            └──────────┘
src     └────┘└──────────┘└─
typ     └────┘└──────────┘└─
doc     └────┘            └─
txt     └────┘            └─
par     └────┘            └─
pid                     
st     └────────────────────
 96  
src  
typ  
doc  
txt  
par  
pid  
st   
 97  @[simp] lemma dist_add_right (g₁ g₂ h : α) : dist (g₁ + h) (g₂ + h) = dist g₁ g₂ :=
id                                               └──┘  └┘     └┘     └──┘ └┘ └┘
src                                               └──┘                  └──┘
typ                                              └──┘  └┘     └┘     └──┘ └┘ └┘
doc    └──┘
 98  by simp [dist_eq_norm]
id            └──────────┘
src     └────┘└──────────┘└─
typ     └────┘└──────────┘└─
doc     └────┘            └─
txt     └────┘            └─
par     └────┘            └─
pid                     
st     └────────────────────
 99  
src  
typ  
doc  
txt  
par  
pid  
st   
100  @[simp] lemma dist_neg_neg (g h : α) : dist (-g) (-h) = dist g h :=
id                                         └──┘        └──┘  
src                                         └──┘          └──┘
typ                                        └──┘        └──┘  
doc    └──┘
101  by simp only [dist_eq_norm, neg_sub_neg, norm_sub_rev]
id                 └──────────┘  └─────────┘  └──────────┘
src     └─────────┘└──────────┘└┘└─────────┘└┘└──────────┘└─
typ     └─────────┘└──────────┘└┘└─────────┘└┘└──────────┘└─
doc     └─────────┘            └┘           └┘            └─
txt     └─────────┘            └┘           └┘            └─
par     └─────────┘            └┘           └┘            └─
pid         └──┘└┘            └┘           └┘            
st     └────────────────────────────────────────────────────
102  
src  
typ  
doc  
txt  
par  
pid  
st   
103  @[simp] lemma dist_sub_left (g h₁ h₂ : α) : dist (g - h₁) (g - h₂) = dist h₁ h₂ :=
id                                              └──┘    └┘     └┘   └──┘ └┘ └┘
src                                              └──┘                  └──┘
typ                                             └──┘    └┘     └┘   └──┘ └┘ └┘
doc    └──┘
104  by simp only [sub_eq_add_neg, dist_add_left, dist_neg_neg]
id                 └────────────┘  └───────────┘  └──────────┘
src     └─────────┘└────────────┘└┘└───────────┘└┘└──────────┘└─
typ     └─────────┘└────────────┘└┘└───────────┘└┘└──────────┘└─
doc     └─────────┘              └┘             └┘            └─
txt     └─────────┘              └┘             └┘            └─
par     └─────────┘              └┘             └┘            └─
pid         └──┘└┘              └┘             └┘            
st     └────────────────────────────────────────────────────────
105  
src  
typ  
doc  
txt  
par  
pid  
st   
106  @[simp] lemma dist_sub_right (g₁ g₂ h : α) : dist (g₁ - h) (g₂ - h) = dist g₁ g₂ :=
id                                               └──┘  └┘     └┘     └──┘ └┘ └┘
src                                               └──┘                  └──┘
typ                                              └──┘  └┘     └┘     └──┘ └┘ └┘
doc    └──┘
107  dist_add_right _ _ _
id   └────────────┘
src  └────────────┘
typ  └────────────┘
108  
109  /-- Triangle inequality for the norm. -/
110  lemma norm_add_le (g h : α) : ∥g + h∥ ≤ ∥g∥ + ∥h∥ :=
id                                      
src                                          
typ                                     
111  by simpa [dist_eq_norm] using dist_triangle g 0 (-h)
id             └──────────┘        └───────────┘     
src     └─────┘└──────────┘└──────┘└───────────┘ └─┘  └─
typ     └─────┘└──────────┘└──────┘└───────────┘└─┘ └─
doc     └─────┘            └──────┘              └─┘   └─
txt     └─────┘            └──────┘              └─┘   └─
par     └─────┘            └──────┘              └─┘   └─
pid                      └────┘              └─┘   
st     └──────────────────────────────────────────────────
112  
src  
typ  
doc  
txt  
par  
pid  
st   
113  lemma norm_add_le_of_le {g₁ g₂ : α} {n₁ n₂ : ℝ} (H₁ : ∥g₁∥ ≤ n₁) (H₂ : ∥g₂∥ ≤ n₂) :
id                                                       └┘  └┘        └┘  └┘
src                                                                        
typ                                                      └┘  └┘        └┘  └┘
114    ∥g₁ + g₂∥ ≤ n₁ + n₂ :=
id     └┘  └┘  └┘  └┘
src               
typ    └┘  └┘  └┘  └┘
115  le_trans (norm_add_le g₁ g₂) (add_le_add H₁ H₂)
id   └──────┘  └─────────┘ └┘ └┘   └────────┘ └┘ └┘
src  └──────┘  └─────────┘         └────────┘
typ  └──────┘  └─────────┘ └┘ └┘   └────────┘ └┘ └┘
doc            └─────────┘
116  
117  lemma dist_add_add_le (g₁ g₂ h₁ h₂ : α) :
id                                        
typ                                       
118    dist (g₁ + g₂) (h₁ + h₂) ≤ dist g₁ h₁ + dist g₂ h₂ :=
id     └──┘  └┘  └┘   └┘  └┘   └──┘ └┘ └┘  └──┘ └┘ └┘
src    └──┘                    └──┘        └──┘
typ    └──┘  └┘  └┘   └┘  └┘   └──┘ └┘ └┘  └──┘ └┘ └┘
119  by simpa only [dist_add_left, dist_add_right] using dist_triangle (g₁ + g₂) (h₁ + g₂) (h₁ + h₂)
id                  └───────────┘  └────────────┘        └───────────┘  └┘            └┘   └┘   └┘
src     └──────────┘└───────────┘└┘└────────────┘└──────┘└───────────┘     └┘      └┘      └─
typ     └──────────┘└───────────┘└┘└────────────┘└──────┘└───────────┘ └┘  └┘    └┘└┘ └┘ └┘└─
doc     └──────────┘             └┘              └──────┘                   └┘      └┘      └─
txt     └──────────┘             └┘              └──────┘                   └┘      └┘      └─
par     └──────────┘             └┘              └──────┘                   └┘      └┘      └─
pid          └──┘└┘             └┘              └────┘                   └┘      └┘      
st     └─────────────────────────────────────────────────────────────────────────────────────────────
120  
src  
typ  
doc  
txt  
par  
pid  
st   
121  lemma dist_add_add_le_of_le {g₁ g₂ h₁ h₂ : α} {d₁ d₂ : ℝ}
id                                                         
src                                                         
typ                                                        
122    (H₁ : dist g₁ h₁ ≤ d₁) (H₂ : dist g₂ h₂ ≤ d₂) :
id           └──┘ └┘ └┘  └┘        └──┘ └┘ └┘  └┘
src          └──┘                  └──┘       
typ          └──┘ └┘ └┘  └┘        └──┘ └┘ └┘  └┘
123    dist (g₁ + g₂) (h₁ + h₂) ≤ d₁ + d₂ :=
id     └──┘  └┘  └┘   └┘  └┘   └┘  └┘
src    └──┘                       
typ    └──┘  └┘  └┘   └┘  └┘   └┘  └┘
124  le_trans (dist_add_add_le g₁ g₂ h₁ h₂) (add_le_add H₁ H₂)
id   └──────┘  └─────────────┘ └┘ └┘ └┘ └┘   └────────┘ └┘ └┘
src  └──────┘  └─────────────┘               └────────┘
typ  └──────┘  └─────────────┘ └┘ └┘ └┘ └┘   └────────┘ └┘ └┘
125  
126  lemma dist_sub_sub_le (g₁ g₂ h₁ h₂ : α) :
id                                        
typ                                       
127    dist (g₁ - g₂) (h₁ - h₂) ≤ dist g₁ h₁ + dist g₂ h₂ :=
id     └──┘  └┘  └┘   └┘  └┘   └──┘ └┘ └┘  └──┘ └┘ └┘
src    └──┘                    └──┘        └──┘
typ    └──┘  └┘  └┘   └┘  └┘   └──┘ └┘ └┘  └──┘ └┘ └┘
128  dist_neg_neg g₂ h₂ ▸ dist_add_add_le _ _ _ _
id   └──────────┘ └┘ └┘  └─────────────┘
src  └──────────┘        └─────────────┘
typ  └──────────┘ └┘ └┘  └─────────────┘
129  
130  lemma dist_sub_sub_le_of_le {g₁ g₂ h₁ h₂ : α} {d₁ d₂ : ℝ}
id                                                         
src                                                         
typ                                                        
131    (H₁ : dist g₁ h₁ ≤ d₁) (H₂ : dist g₂ h₂ ≤ d₂) :
id           └──┘ └┘ └┘  └┘        └──┘ └┘ └┘  └┘
src          └──┘                  └──┘       
typ          └──┘ └┘ └┘  └┘        └──┘ └┘ └┘  └┘
132    dist (g₁ - g₂) (h₁ - h₂) ≤ d₁ + d₂ :=
id     └──┘  └┘  └┘   └┘  └┘   └┘  └┘
src    └──┘                       
typ    └──┘  └┘  └┘   └┘  └┘   └┘  └┘
133  le_trans (dist_sub_sub_le g₁ g₂ h₁ h₂) (add_le_add H₁ H₂)
id   └──────┘  └─────────────┘ └┘ └┘ └┘ └┘   └────────┘ └┘ └┘
src  └──────┘  └─────────────┘               └────────┘
typ  └──────┘  └─────────────┘ └┘ └┘ └┘ └┘   └────────┘ └┘ └┘
134  
135  @[simp] lemma norm_nonneg (g : α) : 0 ≤ ∥g∥ :=
id                                         
src                                          
typ                                        
doc    └──┘
136  by { rw[←dist_zero_right], exact dist_nonneg }
id            └─────────────┘         └─────────┘
src       └──┘└─────────────┘  └────┘└─────────┘
typ       └──┘└─────────────┘  └────┘└─────────┘
doc       └──┘                 └────┘           
txt       └──┘                 └────┘           
par       └──┘                 └────┘           
pid         └┘                                 
st     └────────────────────┘└───────────────────┘└┘
137  
138  lemma norm_eq_zero (g : α) : ∥g∥ = 0 ↔ g = 0 :=
id                                     
src                                       
typ                                    
139  by { rw[←dist_zero_right], exact dist_eq_zero }
id            └─────────────┘         └──────────┘
src       └──┘└─────────────┘  └────┘└──────────┘
typ       └──┘└─────────────┘  └────┘└──────────┘
doc       └──┘                 └────┘            
txt       └──┘                 └────┘            
par       └──┘                 └────┘            
pid         └┘                                  
st     └────────────────────┘└────────────────────┘└┘
140  
141  @[simp] lemma norm_zero : ∥(0:α)∥ = 0 := (norm_eq_zero _).2 rfl
id                                         └──────────┘     └─┘
src                                         └──────────┘     └─┘
typ                                        └──────────┘     └─┘
doc    └──┘
142  
143  lemma norm_sum_le {β} : ∀(s : finset β) (f : β → α), ∥s.sum f∥ ≤ s.sum (λa, ∥ f a ∥) :=
id                                 └────┘             └──┘   └──┘        
src                                └────┘                  └──┘     └──┘           
typ                                └────┘             └──┘   └──┘        
doc                                └────┘
144  finset.le_sum_of_subadditive norm norm_zero norm_add_le
id   └──────────────────────────┘ └──┘ └───────┘ └─────────┘
src  └──────────────────────────┘ └──┘ └───────┘ └─────────┘
typ  └──────────────────────────┘ └──┘ └───────┘ └─────────┘
doc                                              └─────────┘
145  
146  lemma norm_sum_le_of_le {β} (s : finset β) {f : β → α} {n : β → ℝ} (h : ∀ b ∈ s, ∥f b∥ ≤ n b) :
id                                    └────┘                                       
src                                   └────┘                                            
typ                                   └────┘                                       
doc                                   └────┘
147    ∥s.sum f∥ ≤ s.sum n :=
id     └──┘   └──┘ 
src     └──┘     └──┘
typ    └──┘   └──┘ 
148  by { haveI := classical.dec_eq β, exact le_trans (norm_sum_le s f) (finset.sum_le_sum h) }
id                 └──────────────┘         └──────┘  └─────────┘     └───────────────┘ 
src       └───────┘└──────────────┘   └────┘└──────┘ └─────────┘  └┘ └───────────────┘ └┘
typ       └───────┘└──────────────┘  └────┘└──────┘ └─────────┘└┘ └───────────────┘└┘
doc       └───────┘                   └────┘                      └┘                   └┘
txt       └───────┘                   └────┘                      └┘                   └┘
par       └───────┘                   └────┘                      └┘                   └┘
pid            └─┘                                              └┘                   
st     └────────────────────────────┘└───────────────────────────────────────────────────────┘└┘
149  
150  lemma norm_pos_iff (g : α) : 0 < ∥ g ∥ ↔ g ≠ 0 :=
id                                       
src                                         
typ                                      
151  dist_zero_right g ▸ dist_pos
id   └─────────────┘   └──────┘
src  └─────────────┘    └──────┘
typ  └─────────────┘   └──────┘
152  
153  lemma norm_le_zero_iff (g : α) : ∥g∥ ≤ 0 ↔ g = 0 :=
id                                         
src                                           
typ                                        
154  by { rw[←dist_zero_right], exact dist_le_zero }
id            └─────────────┘         └──────────┘
src       └──┘└─────────────┘  └────┘└──────────┘
typ       └──┘└─────────────┘  └────┘└──────────┘
doc       └──┘                 └────┘            
txt       └──┘                 └────┘            
par       └──┘                 └────┘            
pid         └┘                                  
st     └────────────────────┘└────────────────────┘└┘
155  
156  lemma norm_sub_le (g h : α) : ∥g - h∥ ≤ ∥g∥ + ∥h∥ :=
id                                      
src                                          
typ                                     
157  by simpa [dist_eq_norm] using dist_triangle g 0 h
id             └──────────┘        └───────────┘    
src     └─────┘└──────────┘└──────┘└───────────┘ └─┘ 
typ     └─────┘└──────────┘└──────┘└───────────┘└─┘
doc     └─────┘            └──────┘              └─┘ 
txt     └─────┘            └──────┘              └─┘ 
par     └─────┘            └──────┘              └─┘ 
pid                      └────┘              └─┘ 
st     └───────────────────────────────────────────────
158  
src  
typ  
doc  
txt  
par  
pid  
st   
159  lemma norm_sub_le_of_le {g₁ g₂ : α} {n₁ n₂ : ℝ} (H₁ : ∥g₁∥ ≤ n₁) (H₂ : ∥g₂∥ ≤ n₂) :
id                                                       └┘  └┘        └┘  └┘
src                                                                        
typ                                                      └┘  └┘        └┘  └┘
160    ∥g₁ - g₂∥ ≤ n₁ + n₂ :=
id     └┘  └┘  └┘  └┘
src               
typ    └┘  └┘  └┘  └┘
161  le_trans (norm_sub_le g₁ g₂) (add_le_add H₁ H₂)
id   └──────┘  └─────────┘ └┘ └┘   └────────┘ └┘ └┘
src  └──────┘  └─────────┘         └────────┘
typ  └──────┘  └─────────┘ └┘ └┘   └────────┘ └┘ └┘
162  
163  lemma dist_le_norm_add_norm (g h : α) : dist g h ≤ ∥g∥ + ∥h∥ :=
id                                          └──┘      
src                                          └──┘          
typ                                         └──┘      
164  by { rw dist_eq_norm, apply norm_sub_le }
id           └──────────┘        └─────────┘
src       └─┘└──────────┘  └────┘└─────────┘
typ       └─┘└──────────┘  └────┘└─────────┘
doc       └─┘              └────┘           
txt       └─┘              └────┘           
par       └─┘              └────┘           
pid                                       
st     └────────────────┘└──────────────────┘└┘
165  
166  lemma abs_norm_sub_norm_le (g h : α) : abs(∥g∥ - ∥h∥) ≤ ∥g - h∥ :=
id                                         └─┘        
src                                         └─┘            
typ                                        └─┘        
167  by simpa [dist_eq_norm] using abs_dist_sub_le g h 0
id             └──────────┘        └─────────────┘  
src     └─────┘└──────────┘└──────┘└─────────────┘  └──
typ     └─────┘└──────────┘└──────┘└─────────────┘└──
doc     └─────┘            └──────┘                 └──
txt     └─────┘            └──────┘                 └──
par     └─────┘            └──────┘                 └──
pid                      └────┘                 └─
st     └─────────────────────────────────────────────────
168  
src  
typ  
doc  
txt  
par  
pid  
st   
169  lemma norm_sub_norm_le (g h : α) : ∥g∥ - ∥h∥ ≤ ∥g - h∥ :=
id                                           
src                                               
typ                                          
170  le_trans (le_abs_self _) (abs_norm_sub_norm_le g h)
id   └──────┘  └─────────┘     └──────────────────┘  
src  └──────┘  └─────────┘     └──────────────────┘
typ  └──────┘  └─────────┘     └──────────────────┘  
171  
172  lemma dist_norm_norm_le (g h : α) : dist ∥g∥ ∥h∥ ≤ ∥g - h∥ :=
id                                      └──┘      
src                                      └──┘          
typ                                     └──┘      
173  abs_norm_sub_norm_le g h
id   └──────────────────┘  
src  └──────────────────┘
typ  └──────────────────┘  
174  
175  lemma ball_0_eq (ε : ℝ) : ball (0:α) ε = {x | ∥x∥ < ε} :=
id                            └──┘             
src                           └──┘                
typ                           └──┘             
doc                            └──┘
176  set.ext $ assume a, by simp
id   └─────┘          
src  └─────┘                └────
typ  └─────┘               └────
doc                         └────
txt                         └────
par                         └────
pid                             
st                         └─────
177  
src  
typ  
doc  
txt  
par  
pid  
st   
178  lemma norm_le_of_mem_closed_ball {g h : α} {r : ℝ} (H : h ∈ closed_ball g r) :
id                                                           └─────────┘  
src                                                            └─────────┘
typ                                                          └─────────┘  
doc                                                              └─────────┘
179    ∥h∥ ≤ ∥g∥ + r :=
id         
src         
typ        
180  calc
181    ∥h∥ = ∥g + (h - g)∥ : by { congr' 1, abel }
id              
src                         └──────┘  └───┘
typ                     └──────┘  └───┘
doc                               └──────┘  └───┘
txt                               └──────┘  └───┘
par                               └──────┘  └───┘
pid                                           
st                             └─────────┘└─────┘└┘
182    ... ≤ ∥g∥ + ∥h - g∥  : norm_add_le _ _
id                   └─────────┘
src                     └─────────┘
typ                  └─────────┘
doc                           └─────────┘
183    ... ≤ ∥g∥ + r : by { apply add_le_add_left, rw ← dist_eq_norm, exact H }
id                           └─────────────┘       └──────────┘        
src                      └────┘└─────────────┘  └───┘└──────────┘  └────┘ 
typ                    └────┘└─────────────┘  └───┘└──────────┘  └────┘
doc                         └────┘                 └───┘              └────┘ 
txt                         └────┘                 └───┘              └────┘ 
par                         └────┘                 └───┘              └────┘ 
pid                                                 └─┘                    
st                       └──────────────────────┘└─────────────────┘└────────┘└┘
184  
185  lemma norm_lt_of_mem_ball {g h : α} {r : ℝ} (H : h ∈ ball g r) :
id                                                    └──┘  
src                                                     └──┘
typ                                                   └──┘  
doc                                                       └──┘
186    ∥h∥ < ∥g∥ + r :=
id         
src         
typ        
187  calc
188    ∥h∥ = ∥g + (h - g)∥ : by { congr' 1, abel }
id              
src                         └──────┘  └───┘
typ                     └──────┘  └───┘
doc                               └──────┘  └───┘
txt                               └──────┘  └───┘
par                               └──────┘  └───┘
pid                                           
st                             └─────────┘└─────┘└┘
189    ... ≤ ∥g∥ + ∥h - g∥  : norm_add_le _ _
id                   └─────────┘
src                     └─────────┘
typ                  └─────────┘
doc                           └─────────┘
190    ... < ∥g∥ + r : by { apply add_lt_add_left, rw ← dist_eq_norm, exact H }
id                           └─────────────┘       └──────────┘        
src                      └────┘└─────────────┘  └───┘└──────────┘  └────┘ 
typ                    └────┘└─────────────┘  └───┘└──────────┘  └────┘
doc                         └────┘                 └───┘              └────┘ 
txt                         └────┘                 └───┘              └────┘ 
par                         └────┘                 └───┘              └────┘ 
pid                                                 └─┘                    
st                       └──────────────────────┘└─────────────────┘└────────┘└┘
191  
192  theorem normed_group.tendsto_nhds_zero {f : γ → α} {l : filter γ} :
id                                                         └────┘ 
src                                                          └────┘
typ                                                        └────┘ 
193    tendsto f l (𝓝 0) ↔ ∀ ε > 0, ∀ᶠ x in l, ∥ f x ∥ < ε :=
id     └─────┘                 └┘  └┘       
src    └─────┘                   └┘   └┘         
typ    └─────┘                 └┘  └┘       
doc    └─────┘                     └┘   └┘  
194  metric.tendsto_nhds.trans $ forall_congr $ λ ε, forall_congr $ λ εgt0,
id   └─────────────────┘└────┘   └──────────┘       └──────────┘     └──┘
src  └─────────────────┘└────┘   └──────────┘        └──────────┘
typ  └─────────────────┘└────┘   └──────────┘       └──────────┘     └──┘
195  begin
st   └─────
196    simp only [dist_zero_right],
id                └─────────────┘
src    └─────────┘└─────────────┘
typ    └─────────┘└─────────────┘
doc    └─────────┘               
txt    └─────────┘               
par    └─────────┘               
pid        └──┘└┘               
st   ────────────────────────────┘└─
197    exact exists_sets_subset_iff
id           └────────────────────┘
src    └────┘└────────────────────┘
typ    └────┘└────────────────────┘
doc    └────┘                      
txt    └────┘                      
par    └────┘                      
pid                               
st   ──────────────────────────────┘
198  end
st   └─┘
199  
200  section nnnorm
201  
202  /-- Version of the norm taking values in nonnegative reals. -/
203  def nnnorm (a : α) : nnreal := ⟨norm a, norm_nonneg a⟩
id                       └────┘     └──┘   └─────────┘ 
src                       └────┘     └──┘    └─────────┘
typ                      └────┘     └──┘   └─────────┘ 
doc                       └────┘
204  
205  @[simp] lemma coe_nnnorm (a : α) : (nnnorm a : ℝ) = norm a := rfl
id                                      └────┘       └──┘     └─┘
src                                      └────┘        └──┘      └─┘
typ                                     └────┘       └──┘     └─┘
doc    └──┘                              └────┘
206  
207  lemma nndist_eq_nnnorm (a b : α) : nndist a b = nnnorm (a - b) := nnreal.eq $ dist_eq_norm _ _
id                                     └────┘    └────┘         └───────┘   └──────────┘
src                                     └────┘      └────┘           └───────┘   └──────────┘
typ                                    └────┘    └────┘         └───────┘   └──────────┘
doc                                     └────┘       └────┘
208  
209  lemma nnnorm_eq_zero (a : α) : nnnorm a = 0 ↔ a = 0 :=
id                                 └────┘       
src                                 └────┘         
typ                                └────┘       
doc                                 └────┘
210  by simp only [nnreal.eq_iff.symm, nnreal.coe_zero, coe_nnnorm, norm_eq_zero]
id                                     └─────────────┘  └────────┘  └──────────┘
src     └─────────┘                  └┘└─────────────┘└┘└────────┘└┘└──────────┘└─
typ     └─────────┘└────────────────┘└┘└─────────────┘└┘└────────┘└┘└──────────┘└─
doc     └─────────┘                  └┘               └┘          └┘            └─
txt     └─────────┘                  └┘               └┘          └┘            └─
par     └─────────┘                  └┘               └┘          └┘            └─
pid         └──┘└┘                  └┘               └┘          └┘            
st     └──────────────────────────────────────────────────────────────────────────
211  
src  
typ  
doc  
txt  
par  
pid  
st   
212  @[simp] lemma nnnorm_zero : nnnorm (0 : α) = 0 :=
id                               └────┘        
src                              └────┘         
typ                              └────┘        
doc    └──┘                      └────┘
213  nnreal.eq norm_zero
id   └───────┘ └───────┘
src  └───────┘ └───────┘
typ  └───────┘ └───────┘
214  
215  lemma nnnorm_add_le (g h : α) : nnnorm (g + h) ≤ nnnorm g + nnnorm h :=
id                                  └────┘       └────┘   └────┘ 
src                                  └────┘         └────┘    └────┘
typ                                 └────┘       └────┘   └────┘ 
doc                                  └────┘           └────┘     └────┘
216  nnreal.coe_le.2 $ norm_add_le g h
id   └───────────┘    └─────────┘  
src  └───────────┘    └─────────┘
typ  └───────────┘    └─────────┘  
doc                    └─────────┘
217  
218  @[simp] lemma nnnorm_neg (g : α) : nnnorm (-g) = nnnorm g :=
id                                     └────┘     └────┘ 
src                                     └────┘      └────┘
typ                                    └────┘     └────┘ 
doc    └──┘                             └────┘        └────┘
219  nnreal.eq $ norm_neg g
id   └───────┘   └──────┘ 
src  └───────┘   └──────┘
typ  └───────┘   └──────┘ 
220  
221  lemma nndist_nnnorm_nnnorm_le (g h : α) : nndist (nnnorm g) (nnnorm h) ≤ nnnorm (g - h) :=
id                                            └────┘  └────┘    └────┘    └────┘    
src                                            └────┘  └────┘     └────┘     └────┘    
typ                                           └────┘  └────┘    └────┘    └────┘    
doc                                            └────┘  └────┘     └────┘      └────┘
222  nnreal.coe_le.2 $ dist_norm_norm_le g h
id   └───────────┘    └───────────────┘  
src  └───────────┘    └───────────────┘
typ  └───────────┘    └───────────────┘  
223  
224  lemma of_real_norm_eq_coe_nnnorm (x : β) : ennreal.of_real ∥x∥ = (nnnorm x : ennreal) :=
id                                             └─────────────┘    └────┘    └─────┘
src                                             └─────────────┘     └────┘     └─────┘
typ                                            └─────────────┘    └────┘    └─────┘
doc                                             └─────────────┘        └────┘     └─────┘
225  ennreal.of_real_eq_coe_nnreal _
id   └───────────────────────────┘
src  └───────────────────────────┘
typ  └───────────────────────────┘
226  
227  lemma edist_eq_coe_nnnorm (x : β) : edist x 0 = (nnnorm x : ennreal) :=
id                                      └───┘      └────┘    └─────┘
src                                      └───┘       └────┘     └─────┘
typ                                     └───┘      └────┘    └─────┘
doc                                                   └────┘     └─────┘
228  by { rw [edist_dist, dist_eq_norm, _root_.sub_zero, of_real_norm_eq_coe_nnnorm] }
id            └────────┘  └──────────┘  └─────────────┘  └────────────────────────┘
src       └──┘└────────┘└┘└──────────┘└┘└─────────────┘└┘└────────────────────────┘└┘
typ       └──┘└────────┘└┘└──────────┘└┘└─────────────┘└┘└────────────────────────┘└┘
doc       └──┘          └┘            └┘               └┘                          └┘
txt       └──┘          └┘            └┘               └┘                          └┘
par       └──┘          └┘            └┘               └┘                          └┘
pid         └┘          └┘            └┘               └┘                          
st     └───────────────┘└────────────┘└───────────────┘└──────────────────────────┘└┘
229  
230  end nnnorm
231  
232  /-- A submodule of a normed group is also a normed group, with the restriction of the norm.
233  As all instances can be inferred from the submodule `s`, they are put as implicit instead of
234  typeclasses. -/
235  instance submodule.normed_group {𝕜 : Type*} {_ : ring 𝕜}
id                                                    └──┘ 
src                                                   └──┘
typ                                                   └──┘ 
236    {E : Type*} [normed_group E] {_ : module 𝕜 E} (s : submodule 𝕜 E) : normed_group s :=
id                  └──────────┘        └────┘         └───────┘      └──────────┘ 
src                 └──────────┘         └────┘           └───────┘        └──────────┘
typ                 └──────────┘        └────┘         └───────┘      └──────────┘ 
doc                 └──────────┘         └────┘           └───────┘        └──────────┘
237  { norm := λx, norm (x : E),
id                └──┘     
src                └──┘
typ               └──┘     
238    dist_eq := λx y, dist_eq_norm (x : E) (y : E) }
id                    └──────────┘           
src                     └──────────┘
typ                   └──────────┘           
239  
240  /-- normed group instance on the product of two normed groups, using the sup norm. -/
241  instance prod.normed_group : normed_group (α × β) :=
id                                └──────────┘    
src                               └──────────┘    
typ                               └──────────┘    
doc                               └──────────┘
242  { norm := λx, max ∥x.1∥ ∥x.2∥,
id                └─┘    
src                └─┘      
typ               └─┘    
243    dist_eq := assume (x y : α × β),
id                                
src                               
typ                               
244      show max (dist x.1 y.1) (dist x.2 y.2) = (max ∥(x - y).1∥ ∥(x - y).2∥), by simp [dist_eq_norm] }
id            └─┘  └──┘       └──┘        └─┘                        └──────────┘
src           └─┘  └──┘         └──┘          └─┘                      └────┘└──────────┘└┘
typ           └─┘  └──┘       └──┘        └─┘                  └────┘└──────────┘└┘
doc                                                                                 └────┘            └┘
txt                                                                                 └────┘            └┘
par                                                                                 └────┘            └┘
pid                                                                                                 
st                                                                                 └───────────────────┘
245  
246  lemma norm_fst_le (x : α × β) : ∥x.1∥ ≤ ∥x∥ :=
id                                   
src                                      
typ                                  
247  by simp [norm, le_max_left]
id                  └─────────┘
src     └────┘    └┘└─────────┘└─
typ     └────┘    └┘└─────────┘└─
doc     └────┘    └┘           └─
txt     └────┘    └┘           └─
par     └────┘    └┘           └─
pid             └┘           
st     └─────────────────────────
248  
src  
typ  
doc  
txt  
par  
pid  
st   
249  lemma norm_snd_le (x : α × β) : ∥x.2∥ ≤ ∥x∥ :=
id                                   
src                                      
typ                                  
250  by simp [norm, le_max_right]
id                  └──────────┘
src     └────┘    └┘└──────────┘└─
typ     └────┘    └┘└──────────┘└─
doc     └────┘    └┘            └─
txt     └────┘    └┘            └─
par     └────┘    └┘            └─
pid             └┘            
st     └──────────────────────────
251  
src  
typ  
doc  
txt  
par  
pid  
st   
252  /-- normed group instance on the product of finitely many normed groups, using the sup norm. -/
253  instance pi.normed_group {π : ι → Type*} [fintype ι] [∀i, normed_group (π i)] :
id                                            └─────┘       └──────────┘   
src                                            └─────┘         └──────────┘
typ                                           └─────┘       └──────────┘   
doc                                            └─────┘         └──────────┘
254    normed_group (Πi, π i) :=
id     └──────────┘      
src    └──────────┘
typ    └──────────┘      
doc    └──────────┘
255  { norm := λf, ((finset.sup finset.univ (λ b, nnnorm (f b)) : nnreal) : ℝ),
id                  └────────┘ └─────────┘      └────┘        └────┘    
src                  └────────┘ └─────────┘       └────┘          └────┘    
typ                 └────────┘ └─────────┘      └────┘        └────┘    
doc                  └────────┘ └─────────┘       └────┘          └────┘
256    dist_eq := assume x y,
id                        
typ                       
257      congr_arg (coe : nnreal → ℝ) $ congr_arg (finset.sup finset.univ) $ funext $ assume a,
id       └───────┘  └─┘   └────┘       └───────┘  └────────┘ └─────────┘    └────┘          
src      └───────┘  └─┘   └────┘       └───────┘  └────────┘ └─────────┘    └────┘
typ      └───────┘  └─┘   └────┘       └───────┘  └────────┘ └─────────┘    └────┘          
doc                       └────┘                   └────────┘ └─────────┘
258      show nndist (x a) (y a) = nnnorm (x a - y a), from nndist_eq_nnnorm _ _ }
id            └────┘          └────┘              └──────────────┘
src           └────┘              └────┘                  └──────────────┘
typ           └────┘          └────┘              └──────────────┘
doc           └────┘               └────┘
259  
260  /-- The norm of an element in a product space is `≤ r` if and only if the norm of each
261  component is. -/
262  lemma pi_norm_le_iff {π : ι → Type*} [fintype ι] [∀i, normed_group (π i)] {r : ℝ} (hr : 0 ≤ r)
id                                        └─────┘       └──────────┘                      
src                                        └─────┘         └──────────┘                       
typ                                       └─────┘       └──────────┘                      
doc                                        └─────┘         └──────────┘
263    {x : Πi, π i} : ∥x∥ ≤ r ↔ ∀i, ∥x i∥ ≤ r :=
id                            
src                                  
typ                           
264  by { simp only [(dist_zero_right _).symm, dist_pi_le_iff hr], refl }
id                    └─────────────┘          └────────────┘ └┘
src       └─────────┘ └─────────────┘└────────┘└────────────┘    └───┘
typ       └─────────┘ └─────────────┘└────────┘└────────────┘└┘  └───┘
doc       └─────────┘                └────────┘                  └───┘
txt       └─────────┘                └────────┘                  └───┘
par       └─────────┘                └────────┘                  └───┘
pid           └──┘└┘                └────────┘                      
st     └────────────────────────────────────────────────────────┘└─────┘└┘
265  
266  lemma norm_le_pi_norm {π : ι → Type*} [fintype ι] [∀i, normed_group (π i)] (x : Πi, π i) (i : ι) :
id                                         └─────┘       └──────────┘                      
src                                         └─────┘         └──────────┘
typ                                        └─────┘       └──────────┘                      
doc                                         └─────┘         └──────────┘
267    ∥x i∥ ≤ ∥x∥ :=
id        
src          
typ       
268  (pi_norm_le_iff (norm_nonneg x)).1 (le_refl _) i
id    └────────────┘  └─────────┘      └─────┘    
src   └────────────┘  └─────────┘       └─────┘
typ   └────────────┘  └─────────┘      └─────┘    
doc   └────────────┘
269  
270  lemma tendsto_iff_norm_tendsto_zero {f : ι → β} {a : filter ι} {b : β} :
id                                                      └────┘        
src                                                       └────┘
typ                                                     └────┘        
271    tendsto f a (𝓝 b) ↔ tendsto (λ e, ∥ f e - b ∥) a (𝓝 0) :=
id     └─────┘        └─────┘               
src    └─────┘           └─────┘                    
typ    └─────┘        └─────┘               
doc    └─────┘            └─────┘                       
272  by rw tendsto_iff_dist_tendsto_zero ; simp only [(dist_eq_norm _ _).symm]
id         └───────────────────────────┘               └──────────┘
src     └─┘└───────────────────────────┘  └─────────┘ └──────────┘└───────────
typ     └─┘└───────────────────────────┘  └─────────┘ └──────────┘└───────────
doc     └─┘                               └─────────┘             └───────────
txt     └─┘                               └─────────┘             └───────────
par     └─┘                               └─────────┘             └───────────
pid                                          └──┘└┘             └─────────┘
st     └───────────────────────────────────────────────────────────────────────
273  
src  
typ  
doc  
txt  
par  
pid  
st   
274  lemma tendsto_zero_iff_norm_tendsto_zero {f : γ → β} {a : filter γ} :
id                                                           └────┘ 
src                                                            └────┘
typ                                                          └────┘ 
275    tendsto f a (𝓝 0) ↔ tendsto (λ e, ∥ f e ∥) a (𝓝 0) :=
id     └─────┘         └─────┘             
src    └─────┘           └─────┘                 
typ    └─────┘         └─────┘             
doc    └─────┘            └─────┘                   
276  have tendsto f a (𝓝 0) ↔ tendsto (λ e, ∥ f e - 0 ∥) a (𝓝 0) :=
id        └─────┘         └─────┘                
src       └─────┘           └─────┘                    
typ       └─────┘         └─────┘                
doc       └─────┘            └─────┘                       
277    tendsto_iff_norm_tendsto_zero,
id     └───────────────────────────┘
src    └───────────────────────────┘
typ    └───────────────────────────┘
278  by simpa
src     └─────
typ     └─────
doc     └─────
txt     └─────
par     └─────
pid          
st     └──────
279  
src  
typ  
doc  
txt  
par  
pid  
st   
280  lemma lim_norm (x : α) : (λg:α, ∥g - x∥) →_{x} 0 :=
id                                     └─┘
src                                        └─┘ 
typ                                    └─┘
doc                                           └─┘ 
281  tendsto_iff_norm_tendsto_zero.1 (continuous_iff_continuous_at.1 continuous_id x)
id   └───────────────────────────┘   └──────────────────────────┘  └───────────┘ 
src  └───────────────────────────┘   └──────────────────────────┘  └───────────┘
typ  └───────────────────────────┘   └──────────────────────────┘  └───────────┘ 
282  
283  lemma lim_norm_zero : (λg:α, ∥g∥) →_{0} 0 :=
id                                 └─┘ 
src                                  └─┘ 
typ                                └─┘ 
doc                                    └─┘ 
284  by simpa using lim_norm (0:α)
id                  └──────┘    
src     └──────────┘└──────┘ └┘ └─
typ     └──────────┘└──────┘ └┘└─
doc     └──────────┘         └┘ └─
txt     └──────────┘         └┘ └─
par     └──────────┘         └┘ └─
pid          └────┘         └┘ 
st     └───────────────────────────
285  
src  
typ  
doc  
txt  
par  
pid  
st   
286  lemma continuous_norm : continuous (λg:α, ∥g∥) :=
id                           └────────┘       
src                          └────────┘         
typ                          └────────┘       
doc                          └────────┘
287  begin
st   └─────
288    rw continuous_iff_continuous_at,
id        └──────────────────────────┘
src    └─┘└──────────────────────────┘
typ    └─┘└──────────────────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────────────────────────────┘└─
289    intro x,
src    └─────┘
typ    └─────┘
doc    └─────┘
txt    └─────┘
par    └─────┘
pid         └┘
st   ────────┘└─
290    rw [continuous_at, tendsto_iff_dist_tendsto_zero],
id         └───────────┘  └───────────────────────────┘
src    └──┘└───────────┘└┘└───────────────────────────┘
typ    └──┘└───────────┘└┘└───────────────────────────┘
doc    └──┘└───────────┘└┘                             
txt    └──┘             └┘                             
par    └──┘             └┘                             
pid      └┘             └┘                             
st   ──────────────────┘└─────────────────────────────┘└──
291    exact squeeze_zero (λ t, abs_nonneg _) (λ t, abs_norm_sub_norm_le _ _) (lim_norm x)
id           └──────────┘       └────────┘          └──────────────────┘       └──────┘ 
src    └────┘└──────────┘  └──┘└────────┘└──┘  └──┘└──────────────────┘└────┘ └──────┘ └┘
typ    └────┘└──────────┘  └──┘└────────┘└──┘  └──┘└──────────────────┘└────┘ └──────┘└┘
doc    └────┘              └──┘          └──┘  └──┘                    └────┘          └┘
txt    └────┘              └──┘          └──┘  └──┘                    └────┘          └┘
par    └────┘              └──┘          └──┘  └──┘                    └────┘          └┘
pid                       └──┘          └──┘  └──┘                    └────┘          
st   ─────────────────────────────────────────────────────────────────────────────────────┘
292  end
st   └─┘
293  
294  lemma filter.tendsto.norm {β : Type*} {l : filter β} {f : β → α} {a : α} (h : tendsto f l (𝓝 a)) :
id                                              └────┘                         └─────┘     
src                                             └────┘                             └─────┘      
typ                                             └────┘                         └─────┘     
doc                                                                                └─────┘      
295    tendsto (λ x, ∥f x∥) l (𝓝 ∥a∥) :=
id     └─────┘            
src    └─────┘                 
typ    └─────┘            
doc    └─────┘                 
296  tendsto.comp continuous_norm.continuous_at h
id   └──────────┘ └─────────────┘└────────────┘ 
src  └──────────┘ └─────────────┘└────────────┘
typ  └──────────┘ └─────────────┘└────────────┘ 
297  
298  lemma continuous_nnnorm : continuous (nnnorm : α → nnreal) :=
id                             └────────┘  └────┘      └────┘
src                            └────────┘  └────┘       └────┘
typ                            └────────┘  └────┘      └────┘
doc                            └────────┘  └────┘       └────┘
299  continuous_subtype_mk _ continuous_norm
id   └───────────────────┘   └─────────────┘
src  └───────────────────┘   └─────────────┘
typ  └───────────────────┘   └─────────────┘
300  
301  lemma filter.tendsto.nnnorm {β : Type*} {l : filter β} {f : β → α} {a : α} (h : tendsto f l (𝓝 a)) :
id                                                └────┘                         └─────┘     
src                                               └────┘                             └─────┘      
typ                                               └────┘                         └─────┘     
doc                                                                                  └─────┘      
302    tendsto (λ x, nnnorm (f x)) l (𝓝 (nnnorm a)) :=
id     └─────┘      └────┘          └────┘ 
src    └─────┘       └────┘             └────┘
typ    └─────┘      └────┘          └────┘ 
doc    └─────┘       └────┘             └────┘
303  tendsto.comp continuous_nnnorm.continuous_at h
id   └──────────┘ └───────────────┘└────────────┘ 
src  └──────────┘ └───────────────┘└────────────┘
typ  └──────────┘ └───────────────┘└────────────┘ 
304  
305  /-- If `∥y∥→∞`, then we can assume `y≠x` for any fixed `x`. -/
306  lemma ne_mem_of_tendsto_norm_at_top {l : filter γ} {f : γ → α}
id                                            └────┘           
src                                           └────┘
typ                                           └────┘           
307    (h : tendsto (λ y, ∥f y∥) l at_top) (x : α) :
id          └─────┘          └────┘       
src         └─────┘              └────┘
typ         └─────┘          └────┘       
doc         └─────┘                └────┘
308    ∀ᶠ y in l, f y ≠ x :=
id     └┘  └┘     
src    └┘   └┘       
typ    └┘  └┘     
doc    └┘   └┘  
309  begin
st   └─────
310    have : ∀ᶠ y in l, 1 + ∥x∥ ≤ ∥f y∥ := h (mem_at_top (1 + ∥x∥)),
id            └┘   └┘                 └────────┘       
src    └─────┘└┘└─┘└┘ └─┘     └──┘  └────────┘ └┘    └┘
typ    └─────┘└┘└─┘└┘└─┘   └──┘ └────────┘ └┘   └┘
doc    └─────┘└┘└─┘└┘ └─┘         └──┘             └┘    └┘
txt    └─────┘  └─┘    └─┘         └──┘             └┘    └┘
par    └─────┘  └─┘    └─┘         └──┘             └┘    └┘
pid    └───┘└┘  └─┘    └─┘         └──┘             └┘    └┘
st   ──────────────────────────────────────────────────────────────┘└─
311    apply mem_sets_of_superset this,
id           └──────────────────┘ └──┘
src    └────┘└──────────────────┘
typ    └────┘└──────────────────┘└──┘
doc    └────┘                    
txt    └────┘                    
par    └────┘                    
pid                             
st   ────────────────────────────────┘└─
312    assume y hy hxy,
src    └─────────────┘
typ    └─────────────┘
doc    └─────────────┘
txt    └─────────────┘
par    └─────────────┘
pid    └─────────────┘
st   ────────────────┘└─
313    subst x,
id           
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ────────┘└─
314    simp at hy,
src    └────────┘
typ    └────────┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid        └───┘
st   ───────────┘└─
315    exact not_le_of_lt zero_lt_one hy
id           └──────────┘ └─────────┘ └┘
src    └────┘└──────────┘└─────────┘  
typ    └────┘└──────────┘└─────────┘└┘
doc    └────┘                         
txt    └────┘                         
par    └────┘                         
pid                                  
st   ───────────────────────────────────┘
316  end
st   └─┘
317  
318  /-- A normed group is a uniform additive group, i.e., addition and subtraction are uniformly
319  continuous. -/
320  @[priority 100] -- see Note [lower instance priority]
321  instance normed_uniform_group : uniform_add_group α :=
id                                   └───────────────┘ 
src                                  └───────────────┘
typ                                  └───────────────┘ 
doc                                  └───────────────┘
322  begin
st   └─────
323    refine ⟨metric.uniform_continuous_iff.2 $ assume ε hε, ⟨ε / 2, half_pos hε, assume a b h, _⟩⟩,
id             └───────────────────────────┘                         └──────┘
src    └─────┘ └───────────────────────────┘└─┘       └─────┘  └──┘└──────┘  └┘      └─────────┘
typ    └─────┘ └───────────────────────────┘└─┘       └─────┘  └──┘└──────┘  └┘      └─────────┘
doc    └─────┘                              └─┘       └─────┘   └──┘          └┘      └─────────┘
txt    └─────┘                              └─┘       └─────┘   └──┘          └┘      └─────────┘
par    └─────┘                              └─┘       └─────┘   └──┘          └┘      └─────────┘
pid                                        └─┘       └─────┘   └──┘          └┘      └─────────┘
st   ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
324    rw [prod.dist_eq, max_lt_iff, dist_eq_norm, dist_eq_norm] at h,
id         └──────────┘  └────────┘  └──────────┘  └──────────┘
src    └──┘└──────────┘└┘└────────┘└┘└──────────┘└┘└──────────┘└────┘
typ    └──┘└──────────┘└┘└────────┘└┘└──────────┘└┘└──────────┘└────┘
doc    └──┘            └┘          └┘            └┘            └────┘
txt    └──┘            └┘          └┘            └┘            └────┘
par    └──┘            └┘          └┘            └┘            └────┘
pid      └┘            └┘          └┘            └┘            └───┘
st   ─────────────────┘└──────────┘└────────────┘└────────────┘└───┘└─
325    calc dist (a.1 - a.2) (b.1 - b.2) = ∥(a.1 - b.1) - (a.2 - b.2)∥  : by simp [dist_eq_norm]
id     └──┘ └──┘                                                            └──────────┘
src    └──┘ └──┘                                                        └────┘└──────────┘└─
typ    └──┘ └──┘                                                      └────┘└──────────┘└─
doc    └──┘                                                                  └────┘            └─
txt                                                                          └────┘            └─
par                                                                          └────┘            └─
pid                                                                                          
st   ──────────────────────────────────────────────────────────────────────┘└────────────────────
326      ... ≤ ∥a.1 - b.1∥ + ∥a.2 - b.2∥ : norm_sub_le _ _
id                                       └─────────┘
src  ───┘                                └─────────┘
typ  ───┘                                └─────────┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─────────────────────────────────────────────────
327      ... < ε / 2 + ε / 2 : add_lt_add h.1 h.2
id                            └────────┘    
src                           └────────┘     
typ                           └────────┘    
st   ─────────────────────────────────────────────
328      ... = ε : add_halves _
id                └────────┘
src                └────────┘
typ               └────────┘
st   ─────────────────────────┘
329  end
st   ──┘
330  
331  @[priority 100] -- see Note [lower instance priority]
332  instance normed_top_monoid : topological_add_monoid α := by apply_instance -- short-circuit type class inference
id                                └────────────────────┘ 
src                               └────────────────────┘         └───────────────────────────────────────────────────┘
typ                               └────────────────────┘        └───────────────────────────────────────────────────┘
doc                               └────────────────────┘         └───────────────────────────────────────────────────┘
txt                                                              └───────────────────────────────────────────────────┘
par                                                              └───────────────────────────────────────────────────┘
pid                                                                            └─────────────────────────────────────┘
st                                                              └────────────────────────────────────────────────────┘
333  @[priority 100] -- see Note [lower instance priority]
334  instance normed_top_group : topological_add_group α := by apply_instance -- short-circuit type class inference
id                               └───────────────────┘ 
src                              └───────────────────┘         └────────────────────────────────────────────────────
typ                              └───────────────────┘        └────────────────────────────────────────────────────
doc                              └───────────────────┘         └────────────────────────────────────────────────────
txt                                                            └────────────────────────────────────────────────────
par                                                            └────────────────────────────────────────────────────
pid                                                                          └──────────────────────────────────────
st                                                            └─────────────────────────────────────────────────────
335  
src  
typ  
doc  
txt  
par  
pid  
st   
336  end normed_group
337  
338  section normed_ring
339  
340  section prio
341  set_option default_priority 100 -- see Note [default priority]
doc             └──────────────┘
342  /-- A normed ring is a ring endowed with a norm which satisfies the inequality `∥x y∥ ≤ ∥x∥ ∥y∥`. -/
343  class normed_ring (α : Type*) extends has_norm α, ring α, metric_space α :=
id                          └───┘          └──────┘   └──┘   └──────────┘ 
src                                        └──────┘    └──┘    └──────────┘
typ                         └───┘          └──────┘   └──┘   └──────────┘ 
doc                                        └──────┘            └──────────┘
344  (dist_eq : ∀ x y, dist x y = norm (x - y))
id                   └──┘    └──┘    
src                                      
typ                  └──┘    └──┘    
345  (norm_mul : ∀ a b, norm (a * b) ≤ norm a * norm b)
id                    └──┘       └──┘   └──┘ 
src                                         
typ                   └──┘       └──┘   └──┘ 
346  end prio
347  
348  @[priority 100] -- see Note [lower instance priority]
349  instance normed_ring.to_normed_group [β : normed_ring α] : normed_group α := { ..β }
id                                             └─────────┘     └──────────┘         
src                                            └─────────┘      └──────────┘
typ                                            └─────────┘     └──────────┘         
doc                                            └─────────┘      └──────────┘
350  
351  lemma norm_mul_le {α : Type*} [normed_ring α] (a b : α) : (∥a*b∥) ≤ (∥a∥) * (∥b∥) :=
id                                  └─────────┘                       
src                                 └─────────┘                             
typ                                 └─────────┘                       
doc                                 └─────────┘
352  normed_ring.norm_mul _ _
id   └──────────────────┘
src  └──────────────────┘
typ  └──────────────────┘
353  
354  lemma norm_pow_le {α : Type*} [normed_ring α] (a : α) : ∀ {n : ℕ}, 0 < n → ∥a^n∥ ≤ ∥a∥^n
id                                  └─────────┘                             
src                                 └─────────┘                                    
typ                                 └─────────┘                             
doc                                 └─────────┘
355  | 1 h := by simp
src              └───┘
typ              └───┘
doc              └───┘
txt              └───┘
par              └───┘
pid                  
st              └────┘
356  | (n+2) h :=
id      
src      
typ     
357    le_trans (norm_mul_le a (a^(n+1)))
id     └──────┘  └─────────┘     
src    └──────┘  └─────────┘       
typ    └──────┘  └─────────┘     
358             (mul_le_mul (le_refl _)
id               └────────┘  └─────┘
src              └────────┘  └─────┘
typ              └────────┘  └─────┘
359                         (norm_pow_le (nat.succ_pos _)) (norm_nonneg _) (norm_nonneg _))
id                           └─────────┘  └──────────┘      └─────────┘     └─────────┘
src                                       └──────────┘      └─────────┘     └─────────┘
typ                          └─────────┘  └──────────┘      └─────────┘     └─────────┘
360  
361  /-- Normed ring structure on the product of two normed rings, using the sup norm. -/
362  instance prod.normed_ring [normed_ring α] [normed_ring β] : normed_ring (α × β) :=
id                              └─────────┘    └─────────┘     └─────────┘    
src                             └─────────┘     └─────────┘      └─────────┘    
typ                             └─────────┘    └─────────┘     └─────────┘    
doc                             └─────────┘     └─────────┘      └─────────┘
363  { norm_mul := assume x y,
id                         
typ                        
364    calc
365      ∥x * y∥ = ∥(x.1*y.1, x.2*y.2)∥ : rfl
id                      └─┘
src                           └─┘
typ                     └─┘
366          ... = (max ∥x.1*y.1∥  ∥x.2*y.2∥) : rfl
id                  └─┘           └─┘
src                 └─┘               └─┘
typ                 └─┘           └─┘
367          ... ≤ (max (∥x.1∥*∥y.1∥) (∥x.2∥*∥y.2∥)) :
id                  └─┘         
src                 └─┘             
typ                 └─┘         
368            max_le_max (norm_mul_le (x.1) (y.1)) (norm_mul_le (x.2) (y.2))
id             └────────┘  └─────────┘           └─────────┘      
src            └────────┘  └─────────┘             └─────────┘        
typ            └────────┘  └─────────┘           └─────────┘      
369          ... = (max (∥x.1∥*∥y.1∥) (∥y.2∥*∥x.2∥)) : by simp[mul_comm]
id                  └─┘                      └──────┘
src                 └─┘                     └───┘└──────┘└─
typ                 └─┘                 └───┘└──────┘└─
doc                                                       └───┘        └─
txt                                                       └───┘        └─
par                                                       └───┘        └─
pid                                                                   
st                                                       └───────────────
370          ... ≤ (max (∥x.1∥) (∥x.2∥)) * (max (∥y.2∥) (∥y.1∥)) : by { apply max_mul_mul_le_max_mul_max; simp [norm_nonneg] }
id                  └─┘            └─┘                       └────────────────────────┘        └─────────┘
src  ───────┘       └─┘              └─┘                   └────┘└────────────────────────┘  └────┘└─────────┘└┘
typ  ───────┘       └─┘            └─┘                 └────┘└────────────────────────┘  └────┘└─────────┘└┘
doc  ───────┘                                                           └────┘                            └────┘           └┘
txt  ───────┘                                                           └────┘                            └────┘           └┘
par  ───────┘                                                           └────┘                            └────┘           └┘
pid  ───────┘                                                                                                           
st   ───────┘                                                        └──────────────────────────────────────────────────────┘└┘
371          ... = (max (∥x.1∥) (∥x.2∥)) * (max (∥y.1∥) (∥y.2∥)) : by simp[max_comm]
id                  └─┘            └─┘                    └──────┘
src                 └─┘              └─┘                 └───┘└──────┘└─
typ                 └─┘            └─┘               └───┘└──────┘└─
doc                                                                   └───┘        └─
txt                                                                   └───┘        └─
par                                                                   └───┘        └─
pid                                                                               
st                                                                   └───────────────
372          ... = (∥x∥*∥y∥) : rfl,
id                      └─┘
src  ───────┘             └─┘
typ  ───────┘           └─┘
doc  ───────┘
txt  ───────┘
par  ───────┘
pid  ───────┘
st   ───────┘
373    ..prod.normed_group }
id       └───────────────┘
src      └───────────────┘
typ      └───────────────┘
doc      └───────────────┘
374  end normed_ring
375  
376  @[priority 100] -- see Note [lower instance priority]
377  instance normed_ring_top_monoid [normed_ring α] : topological_monoid α :=
id                                    └─────────┘     └────────────────┘ 
src                                   └─────────┘      └────────────────┘
typ                                   └─────────┘     └────────────────┘ 
doc                                   └─────────┘      └────────────────┘
378  ⟨ continuous_iff_continuous_at.2 $ λ x, tendsto_iff_norm_tendsto_zero.2 $
id     └──────────────────────────┘        └───────────────────────────┘
src    └──────────────────────────┘         └───────────────────────────┘
typ    └──────────────────────────┘        └───────────────────────────┘
379      have ∀ e : α × α, e.fst * e.snd - x.fst * x.snd =
id                      └──┘  └──┘  └──┘  └──┘ 
src                        └──┘   └──┘   └──┘   └──┘ 
typ                     └──┘  └──┘  └──┘  └──┘ 
380        e.fst * e.snd - e.fst * x.snd + (e.fst * x.snd - x.fst * x.snd), by intro; rw sub_add_sub_cancel,
id         └──┘  └──┘  └──┘  └──┘   └──┘  └──┘  └──┘  └──┘                └────────────────┘
src         └──┘   └──┘   └──┘   └──┘    └──┘   └──┘   └──┘   └──┘      └───┘  └─┘└────────────────┘
typ        └──┘  └──┘  └──┘  └──┘   └──┘  └──┘  └──┘  └──┘      └───┘  └─┘└────────────────┘
doc                                                                            └───┘  └─┘
txt                                                                            └───┘  └─┘
par                                                                            └───┘  └─┘
pid                                                                                     
st                                                                            └─────────┘└────────────────┘
381      begin
st       └─────
382        apply squeeze_zero,
id               └──────────┘
src        └────┘└──────────┘
typ        └────┘└──────────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ───────────────────────┘└─
383        { intro, apply norm_nonneg },
id                        └─────────┘
src          └───┘  └────┘└─────────┘
typ          └───┘  └────┘└─────────┘
doc          └───┘  └────┘           
txt          └───┘  └────┘           
par          └───┘  └────┘           
pid                                 
st   ───────┘└───┘└──────────────────┘└┘
384        { simp only [this], intro, apply norm_add_le },
id                      └──┘                └─────────┘
src          └─────────┘      └───┘  └────┘└─────────┘
typ          └─────────┘└──┘  └───┘  └────┘└─────────┘
doc          └─────────┘      └───┘  └────┘└─────────┘
txt          └─────────┘      └───┘  └────┘           
par          └─────────┘      └───┘  └────┘           
pid              └──┘└┘                             
st   ───────┘└──────────────┘└─────┘└──────────────────┘└┘
385        { rw ←zero_add (0 : ℝ), apply tendsto.add,
id               └──────┘                └─────────┘
src          └──┘└──────┘ └──┘   └────┘└─────────┘
typ          └──┘└──────┘ └──┘   └────┘└─────────┘
doc          └──┘         └──┘   └────┘
txt          └──┘         └──┘   └────┘
par          └──┘         └──┘   └────┘
pid            └┘         └──┘        
st   ───────────────────────────┘└─────────────────┘└─
386          { apply squeeze_zero,
id                   └──────────┘
src            └────┘└──────────┘
typ            └────┘└──────────┘
doc            └────┘
txt            └────┘
par            └────┘
pid                 
st   ─────────┘└────────────────┘└─
387            { intro, apply norm_nonneg },
id                            └─────────┘
src              └───┘  └────┘└─────────┘
typ              └───┘  └────┘└─────────┘
doc              └───┘  └────┘           
txt              └───┘  └────┘           
par              └───┘  └────┘           
pid                                     
st   ───────────┘└───┘└──────────────────┘└┘
388            { intro t, show ∥t.fst * t.snd - t.fst * x.snd∥ ≤ ∥t.fst∥ * ∥t.snd - x.snd∥,
id                                                           └───┘     └───┘   └───┘
src              └─────┘  └───┘                      └───┘   └───┘ └───┘
typ              └─────┘  └───┘                      └───┘   └───┘ └───┘
doc              └─────┘  └───┘                                         
txt              └─────┘  └───┘                                         
par              └─────┘  └───┘                                         
pid                   └┘  └───┘                                         
st   ───────────┘└─────┘└────────────────────────────────────────────────────────────────┘└─
389              rw ←mul_sub, apply norm_mul_le },
id                   └─────┘        └─────────┘
src              └──┘└─────┘  └────┘└─────────┘
typ              └──┘└─────┘  └────┘└─────────┘
doc              └──┘         └────┘           
txt              └──┘         └────┘           
par              └──┘         └────┘           
pid                └┘                         
st   ──────────────────────┘└──────────────────┘└┘
390            { rw ←mul_zero (∥x.fst∥), apply tendsto.mul,
id                   └──────┘   └───┘          └─────────┘
src              └──┘└──────┘  └───┘   └────┘└─────────┘
typ              └──┘└──────┘  └───┘   └────┘└─────────┘
doc              └──┘                  └────┘
txt              └──┘                  └────┘
par              └──┘                  └────┘
pid                └┘                       
st   ─────────────────────────────────┘└─────────────────┘└─
391              { apply continuous_iff_continuous_at.1,
id                       └──────────────────────────┘
src                └────┘└──────────────────────────┘└┘
typ                └────┘└──────────────────────────┘└┘
doc                └────┘                            └┘
txt                └────┘                            └┘
par                └────┘                            └┘
pid                                                 └┘
st   ─────────────┘└──────────────────────────────────┘└─
392                apply continuous_norm.comp continuous_fst },
id                       └──────────────────┘ └────────────┘
src                └────┘└──────────────────┘└────────────┘
typ                └────┘└──────────────────┘└────────────┘
doc                └────┘                                  
txt                └────┘                                  
par                └────┘                                  
pid                                                       
st   ───────────────────────────────────────────────────────┘└┘
393              { apply tendsto_iff_norm_tendsto_zero.1,
id                       └───────────────────────────┘
src                └────┘└───────────────────────────┘└┘
typ                └────┘└───────────────────────────┘└┘
doc                └────┘                             └┘
txt                └────┘                             └┘
par                └────┘                             └┘
pid                                                  └┘
st   ──────────────────────────────────────────────────┘└─
394                apply continuous_iff_continuous_at.1,
id                       └──────────────────────────┘
src                └────┘└──────────────────────────┘└┘
typ                └────┘└──────────────────────────┘└┘
doc                └────┘                            └┘
txt                └────┘                            └┘
par                └────┘                            └┘
pid                                                 └┘
st   ─────────────────────────────────────────────────┘└─
395                apply continuous_snd }}},
id                       └────────────┘
src                └────┘└────────────┘
typ                └────┘└────────────┘
doc                └────┘              
txt                └────┘              
par                └────┘              
pid                                   
st   ──────────────────────────────────┘└──┘
396          { apply squeeze_zero,
id                   └──────────┘
src            └────┘└──────────┘
typ            └────┘└──────────┘
doc            └────┘
txt            └────┘
par            └────┘
pid                 
st   ───────────────────────────┘└─
397            { intro, apply norm_nonneg },
id                            └─────────┘
src              └───┘  └────┘└─────────┘
typ              └───┘  └────┘└─────────┘
doc              └───┘  └────┘           
txt              └───┘  └────┘           
par              └───┘  └────┘           
pid                                     
st   ───────────┘└───┘└──────────────────┘└┘
398            { intro t, show ∥t.fst * x.snd - x.fst * x.snd∥ ≤ ∥t.fst - x.fst∥ * ∥x.snd∥,
id                                                                └───┘   └───┘     └───┘
src              └─────┘  └───┘                           └───┘ └───┘   └───┘
typ              └─────┘  └───┘                           └───┘ └───┘   └───┘
doc              └─────┘  └───┘                                        
txt              └─────┘  └───┘                                        
par              └─────┘  └───┘                                        
pid                   └┘  └───┘                                        
st   ───────────┘└─────┘└────────────────────────────────────────────────────────────────┘└─
399              rw ←sub_mul, apply norm_mul_le },
id                   └─────┘        └─────────┘
src              └──┘└─────┘  └────┘└─────────┘
typ              └──┘└─────┘  └────┘└─────────┘
doc              └──┘         └────┘           
txt              └──┘         └────┘           
par              └──┘         └────┘           
pid                └┘                         
st   ──────────────────────┘└──────────────────┘└┘
400            { rw ←zero_mul (∥x.snd∥), apply tendsto.mul,
id                   └──────┘   └───┘          └─────────┘
src              └──┘└──────┘  └───┘   └────┘└─────────┘
typ              └──┘└──────┘  └───┘   └────┘└─────────┘
doc              └──┘                  └────┘
txt              └──┘                  └────┘
par              └──┘                  └────┘
pid                └┘                       
st   ─────────────────────────────────┘└─────────────────┘└─
401              { apply tendsto_iff_norm_tendsto_zero.1,
id                       └───────────────────────────┘
src                └────┘└───────────────────────────┘└┘
typ                └────┘└───────────────────────────┘└┘
doc                └────┘                             └┘
txt                └────┘                             └┘
par                └────┘                             └┘
pid                                                  └┘
st   ─────────────┘└───────────────────────────────────┘└─
402                apply continuous_iff_continuous_at.1,
id                       └──────────────────────────┘
src                └────┘└──────────────────────────┘└┘
typ                └────┘└──────────────────────────┘└┘
doc                └────┘                            └┘
txt                └────┘                            └┘
par                └────┘                            └┘
pid                                                 └┘
st   ─────────────────────────────────────────────────┘└─
403                apply continuous_fst },
id                       └────────────┘
src                └────┘└────────────┘
typ                └────┘└────────────┘
doc                └────┘              
txt                └────┘              
par                └────┘              
pid                                   
st   ──────────────────────────────────┘└┘
404              { apply tendsto_const_nhds }}}}
id                       └────────────────┘
src                └────┘└────────────────┘
typ                └────┘└────────────────┘
doc                └────┘                  
txt                └────┘                  
par                └────┘                  
pid                                       
st   ──────────────────────────────────────┘└────
405      end ⟩
st   ──────┘
406  
407  /-- A normed ring is a topological ring. -/
408  @[priority 100] -- see Note [lower instance priority]
409  instance normed_top_ring [normed_ring α] : topological_ring α :=
id                             └─────────┘     └──────────────┘ 
src                            └─────────┘      └──────────────┘
typ                            └─────────┘     └──────────────┘ 
doc                            └─────────┘      └──────────────┘
410  ⟨ continuous_iff_continuous_at.2 $ λ x, tendsto_iff_norm_tendsto_zero.2 $
id     └──────────────────────────┘        └───────────────────────────┘
src    └──────────────────────────┘         └───────────────────────────┘
typ    └──────────────────────────┘        └───────────────────────────┘
411      have ∀ e : α, -e - -x = -(e - x), by intro; simp,
id                           
src                                     └───┘  └──┘
typ                                └───┘  └──┘
doc                                           └───┘  └──┘
txt                                           └───┘  └──┘
par                                           └───┘  └──┘
st                                           └──────────┘
412      by simp only [this, norm_neg]; apply lim_norm ⟩
id                     └──┘  └──────┘         └──────┘
src         └─────────┘    └┘└──────┘  └────┘└──────┘
typ         └─────────┘└──┘└┘└──────┘  └────┘└──────┘
doc         └─────────┘    └┘          └────┘        
txt         └─────────┘    └┘          └────┘        
par         └─────────┘    └┘          └────┘        
pid             └──┘└┘    └┘                       
st         └──────────────────────────────────────────┘
413  
414  section prio
415  set_option default_priority 100 -- see Note [default priority]
doc             └──────────────┘
416  /-- A normed field is a field with a norm satisfying ∥x y∥ = ∥x∥ ∥y∥. -/
417  class normed_field (α : Type*) extends has_norm α, discrete_field α, metric_space α :=
id                           └───┘          └──────┘   └────────────┘   └──────────┘ 
src                                         └──────┘    └────────────┘    └──────────┘
typ                          └───┘          └──────┘   └────────────┘   └──────────┘ 
doc                                         └──────┘                      └──────────┘
418  (dist_eq : ∀ x y, dist x y = norm (x - y))
id                   └──┘    └──┘    
src                                      
typ                  └──┘    └──┘    
419  (norm_mul' : ∀ a b, norm (a * b) = norm a * norm b)
id                     └──┘       └──┘   └──┘ 
src                                          
typ                    └──┘       └──┘   └──┘ 
420  
421  /-- A nondiscrete normed field is a normed field in which there is an element of norm different from
422  `0` and `1`. This makes it possible to bring any element arbitrarily close to `0` by multiplication
423  by the powers of any element, and thus to relate algebra and topology. -/
424  class nondiscrete_normed_field (α : Type*) extends normed_field α :=
id                                       └───┘          └──────────┘ 
src                                                     └──────────┘
typ                                      └───┘          └──────────┘ 
doc                                                     └──────────┘
425  (non_trivial : ∃x:α, 1<∥x∥)
id                      
src                       
typ                     
426  end prio
427  
428  @[priority 100] -- see Note [lower instance priority]
429  instance normed_field.to_normed_ring [i : normed_field α] : normed_ring α :=
id                                             └──────────┘     └─────────┘ 
src                                            └──────────┘      └─────────┘
typ                                            └──────────┘     └─────────┘ 
doc                                            └──────────┘      └─────────┘
430  { norm_mul := by finish [i.norm_mul'], ..i }
id                                            
src                   └──────┘           
typ                   └──────┘└─────────┘    
doc                   └──────┘           
txt                   └──────┘           
par                   └──────┘           
pid                         └┘           
st                   └───────────────────┘
431  
432  namespace normed_field
433  @[simp] lemma norm_one {α : Type*} [normed_field α] : ∥(1 : α)∥ = 1 :=
id                                       └──────────┘            
src                                      └──────────┘              
typ                                      └──────────┘            
doc    └──┘                              └──────────┘
434  have  ∥(1 : α)∥ * ∥(1 : α)∥ = ∥(1 : α)∥ * 1, by calc
id                                       └──┘
src                                         └──┘
typ                                      └──┘
doc                                                  └──┘
st                                                  └─────
435   ∥(1 : α)∥ * ∥(1 : α)∥ = ∥(1 : α) * (1 : α)∥ : by rw normed_field.norm_mul'
id                                                     └────────────────────┘
src                                                 └─┘└────────────────────┘
typ                                                 └─┘└────────────────────┘
doc                                                    └─┘                      
txt                                                    └─┘                      
par                                                    └─┘                      
pid                                                                            
st   ────────────────────────────────────────────────┘└──────────────────────────
436                    ... = ∥(1 : α)∥ * 1 : by simp,
id                                 
src  ─────────────────┘                         └──┘
typ  ─────────────────┘                        └──┘
doc  ─────────────────┘                         └──┘
txt  ─────────────────┘                         └──┘
par  ─────────────────┘                         └──┘
pid  ─────────────────┘
st   ─────────────────┘└──────────────────────┘└───┘
437  eq_of_mul_eq_mul_left (ne_of_gt ((norm_pos_iff _).2 (by simp))) this
id   └───────────────────┘  └──────┘   └──────────┘                 └──┘
src  └───────────────────┘  └──────┘   └──────────┘         └──┘
typ  └───────────────────┘  └──────┘   └──────────┘         └──┘    └──┘
doc                                                          └──┘
txt                                                          └──┘
par                                                          └──┘
st                                                          └───┘
438  
439  @[simp] lemma norm_mul [normed_field α] (a b : α) : ∥a * b∥ = ∥a∥ * ∥b∥ :=
id                           └──────────┘                    
src                          └──────────┘                          
typ                          └──────────┘                    
doc    └──┘                  └──────────┘
440  normed_field.norm_mul' a b
id   └────────────────────┘  
src  └────────────────────┘
typ  └────────────────────┘  
441  
442  instance normed_field.is_monoid_hom_norm [normed_field α] : is_monoid_hom (norm : α → ℝ) :=
id                                             └──────────┘     └───────────┘  └──┘      
src                                            └──────────┘      └───────────┘  └──┘       
typ                                            └──────────┘     └───────────┘  └──┘      
doc                                            └──────────┘      └───────────┘
443  { map_one := norm_one, map_mul := norm_mul }
id                └──────┘             └──────┘
src               └──────┘             └──────┘
typ               └──────┘             └──────┘
444  
445  @[simp] lemma norm_pow [normed_field α] (a : α) : ∀ (n : ℕ), ∥a^n∥ = ∥a∥^n :=
id                           └──────────┘                        
src                          └──────────┘                             
typ                          └──────────┘                        
doc    └──┘                  └──────────┘
446  is_monoid_hom.map_pow norm a
id   └───────────────────┘ └──┘ 
src  └───────────────────┘ └──┘
typ  └───────────────────┘ └──┘ 
447  
448  @[simp] lemma norm_prod {β : Type*} [normed_field α] (s : finset β) (f : β → α) :
id                                        └──────────┘        └────┘           
src                                       └──────────┘         └────┘
typ                                       └──────────┘        └────┘           
doc    └──┘                               └──────────┘         └────┘
449    ∥s.prod f∥ = s.prod (λb, ∥f b∥) :=
id     └───┘   └───┘      
src     └───┘     └───┘         
typ    └───┘   └───┘      
doc      └───┘       └───┘
450  eq.symm (s.prod_hom norm)
id   └─────┘  └───────┘ └──┘
src  └─────┘   └───────┘ └──┘
typ  └─────┘  └───────┘ └──┘
451  
452  @[simp] lemma norm_div {α : Type*} [normed_field α] (a b : α) : ∥a/b∥ = ∥a∥/∥b∥ :=
id                                       └──────────┘                
src                                      └──────────┘                      
typ                                      └──────────┘                
doc    └──┘                              └──────────┘
453  if hb : b = 0 then by simp [hb] else
id   └┘                        └┘
src  └┘                   └────┘  └┘
typ  └┘                  └────┘└┘└┘
doc                        └────┘  └┘
txt                        └────┘  └┘
par                        └────┘  └┘
pid                              
st                        └─────────┘
454  begin
st   └─────
455    apply eq_div_of_mul_eq,
id           └──────────────┘
src    └────┘└──────────────┘
typ    └────┘└──────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ───────────────────────┘└─
456    { apply ne_of_gt, apply (norm_pos_iff _).mpr hb },
id             └──────┘         └──────────┘        └┘
src      └────┘└──────┘  └────┘ └──────────┘└──────┘  
typ      └────┘└──────┘  └────┘ └──────────┘└──────┘└┘
doc      └────┘          └────┘             └──────┘  
txt      └────┘          └────┘             └──────┘  
par      └────┘          └────┘             └──────┘  
pid                                       └──────┘  
st   ───┘└────────────┘└──────────────────────────────┘└┘
457    { rw [←normed_field.norm_mul, div_mul_cancel _ hb] }
id            └───────────────────┘  └────────────┘   └┘
src      └───┘└───────────────────┘└┘└────────────┘└─┘  └┘
typ      └───┘└───────────────────┘└┘└────────────┘└─┘└┘└┘
doc      └───┘                     └┘              └─┘  └┘
txt      └───┘                     └┘              └─┘  └┘
par      └───┘                     └┘              └─┘  └┘
pid        └─┘                     └┘              └─┘  
st   ─────────────────────────────┘└───────────────────┘└─
458  end
id   └─┘
src  └─┘
typ  └─┘
st   ──┘
459  
460  @[simp] lemma norm_inv {α : Type*} [normed_field α] (a : α) : ∥a⁻¹∥ = ∥a∥⁻¹ :=
id                                       └──────────┘            └┘  └┘
src                                      └──────────┘               └┘   └┘
typ                                      └──────────┘            └┘  └┘
doc    └──┘                              └──────────┘
461  by simp only [inv_eq_one_div, norm_div, norm_one]
id                 └────────────┘  └──────┘  └──────┘
src     └─────────┘└────────────┘└┘└──────┘└┘└──────┘└─
typ     └─────────┘└────────────┘└┘└──────┘└┘└──────┘└─
doc     └─────────┘              └┘        └┘        └─
txt     └─────────┘              └┘        └┘        └─
par     └─────────┘              └┘        └┘        └─
pid         └──┘└┘              └┘        └┘        
st     └───────────────────────────────────────────────
462  
src  
typ  
doc  
txt  
par  
pid  
st   
463  @[simp] lemma norm_fpow {α : Type*} [normed_field α] (a : α) : ∀n : ℤ,
id                                        └──────────┘                
src                                       └──────────┘                   
typ                                       └──────────┘                
doc    └──┘                               └──────────┘
464    ∥a^n∥ = ∥a∥^n
id       
src         
typ      
465  | (n : ℕ) := norm_pow a n
id              └──────┘ 
src              └──────┘
typ             └──────┘ 
466  | -[1+ n] := by simp [fpow_neg_succ_of_nat]
id     └──┘               └──────────────────┘
src    └──┘         └────┘└──────────────────┘└─
typ    └──┘         └────┘└──────────────────┘└─
doc                  └────┘                    └─
txt                  └────┘                    └─
par                  └────┘                    └─
pid                                          
st                  └────────────────────────────
467  
src  
typ  
doc  
txt  
par  
pid  
st   
468  lemma exists_one_lt_norm (α : Type*) [i : nondiscrete_normed_field α] : ∃x : α, 1 < ∥x∥ :=
id                                             └──────────────────────┘             
src                                            └──────────────────────┘                
typ                                            └──────────────────────┘             
doc                                            └──────────────────────┘
469  i.non_trivial
id   └──────────┘
src   └──────────┘
typ  └──────────┘
470  
471  lemma exists_norm_lt_one (α : Type*) [nondiscrete_normed_field α] : ∃x : α, 0 < ∥x∥ ∧ ∥x∥ < 1 :=
id                                         └──────────────────────┘                
src                                        └──────────────────────┘                    
typ                                        └──────────────────────┘                
doc                                        └──────────────────────┘
472  begin
st   └─────
473    rcases exists_one_lt_norm α with ⟨y, hy⟩,
id            └────────────────┘ 
src    └─────┘└────────────────┘ └───────────┘
typ    └─────┘└────────────────┘└───────────┘
doc    └─────┘                   └───────────┘
txt    └─────┘                   └───────────┘
par    └─────┘                   └───────────┘
pid                             └───────────┘
st   ─────────────────────────────────────────┘└─
474    refine ⟨y⁻¹, _, _⟩,
id             └┘
src    └─────┘  └┘└─────┘
typ    └─────┘ └┘└─────┘
doc    └─────┘    └─────┘
txt    └─────┘    └─────┘
par    └─────┘    └─────┘
pid              └─────┘
st   ───────────────────┘└─
475    { simp only [inv_eq_zero, ne.def, norm_pos_iff],
id                  └─────────┘  └────┘  └──────────┘
src      └─────────┘└─────────┘└┘└────┘└┘└──────────┘
typ      └─────────┘└─────────┘└┘└────┘└┘└──────────┘
doc      └─────────┘           └┘      └┘            
txt      └─────────┘           └┘      └┘            
par      └─────────┘           └┘      └┘            
pid          └──┘└┘           └┘      └┘            
st   ───┘└───────────────────────────────────────────┘└─
476      assume h,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───────────┘└─
477      rw ← norm_eq_zero at h,
id            └──────────┘
src      └───┘└──────────┘└───┘
typ      └───┘└──────────┘└───┘
doc      └───┘            └───┘
txt      └───┘            └───┘
par      └───┘            └───┘
pid        └─┘            └───┘
st   ─────────────────────────┘└─
478      rw h at hy,
id          
src      └─┘ └────┘
typ      └─┘└────┘
doc      └─┘ └────┘
txt      └─┘ └────┘
par      └─┘ └────┘
pid         └────┘
st   ─────────────┘└─
479      exact lt_irrefl _ (lt_trans zero_lt_one hy) },
id             └───────┘    └──────┘ └─────────┘ └┘
src      └────┘└───────┘└─┘ └──────┘└─────────┘  └┘
typ      └────┘└───────┘└─┘ └──────┘└─────────┘└┘└┘
doc      └────┘         └─┘                      └┘
txt      └────┘         └─┘                      └┘
par      └────┘         └─┘                      └┘
pid                    └─┘                      
st   ───────────────────────────────────────────────┘└┘
480    { simp [inv_lt_one hy] }
id             └────────┘ └┘
src      └────┘└────────┘  └┘
typ      └────┘└────────┘└┘└┘
doc      └────┘            └┘
txt      └────┘            └┘
par      └────┘            └┘
pid                      
st   ────────────────────────┘└─
481  end
st   ──┘
482  
483  lemma exists_lt_norm (α : Type*) [nondiscrete_normed_field α]
id                                     └──────────────────────┘ 
src                                    └──────────────────────┘
typ                                    └──────────────────────┘ 
doc                                    └──────────────────────┘
484    (r : ℝ) : ∃ x : α, r < ∥x∥ :=
id                      
src                        
typ                     
485  let ⟨w, hw⟩ := exists_one_lt_norm α in
id   └─┘    └┘     └────────────────┘ 
src                 └────────────────┘
typ  └─┘    └┘     └────────────────┘ 
486  let ⟨n, hn⟩ := pow_unbounded_of_one_lt r hw in
id   └─┘           └─────────────────────┘ 
src                 └─────────────────────┘
typ  └─┘           └─────────────────────┘ 
487  ⟨w^n, by rwa norm_pow⟩
id               └──────┘
src          └──┘└──────┘
typ          └──┘└──────┘
doc           └──┘
txt           └──┘
par           └──┘
pid              
st           └───────────┘
488  
489  lemma exists_norm_lt (α : Type*) [nondiscrete_normed_field α]
id                                     └──────────────────────┘ 
src                                    └──────────────────────┘
typ                                    └──────────────────────┘ 
doc                                    └──────────────────────┘
490    {r : ℝ} (hr : 0 < r) : ∃ x : α, 0 < ∥x∥ ∧ ∥x∥ < r :=
id                                      
src                                        
typ                                     
491  let ⟨w, hw⟩ := exists_one_lt_norm α in
id   └─┘    └┘     └────────────────┘ 
src                 └────────────────┘
typ  └─┘    └┘     └────────────────┘ 
492  let ⟨n, hle, hlt⟩ := exists_int_pow_near' hr hw in
id   └─┘                 └──────────────────┘ └┘
src                       └──────────────────┘
typ  └─┘                 └──────────────────┘ └┘
doc                       └──────────────────┘
493  ⟨w^n, by { rw norm_fpow; exact fpow_pos_of_pos (lt_trans zero_lt_one hw) _},
id                └───────┘        └─────────────┘  └──────┘ └─────────┘ └┘
src            └─┘└───────┘  └────┘└─────────────┘ └──────┘└─────────┘  └─┘
typ            └─┘└───────┘  └────┘└─────────────┘ └──────┘└─────────┘└┘└─┘
doc             └─┘           └────┘                                     └─┘
txt             └─┘           └────┘                                     └─┘
par             └─┘           └────┘                                     └─┘
pid                                                                    └─┘
st           └────────────────────────────────────────────────────────────────┘└┘
494  by rwa norm_fpow⟩
id          └───────┘
src     └──┘└───────┘
typ     └──┘└───────┘
doc     └──┘
txt     └──┘
par     └──┘
pid        
st     └────────────┘
495  
496  lemma tendsto_inv [normed_field α] {r : α} (r0 : r ≠ 0) : tendsto (λq, q⁻¹) (𝓝 r) (𝓝 r⁻¹) :=
id                      └──────────┘                       └─────┘     └┘        └┘
src                     └──────────┘                          └─────┘       └┘          └┘
typ                     └──────────┘                       └─────┘     └┘        └┘
doc                     └──────────┘                           └─────┘                 
497  begin
st   └─────
498    refine metric.tendsto_nhds.2 (λε εpos, _),
id            └─────────────────┘
src    └─────┘└─────────────────┘└─┘  └────────┘
typ    └─────┘└─────────────────┘└─┘  └────────┘
doc    └─────┘                   └─┘  └────────┘
txt    └─────┘                   └─┘  └────────┘
par    └─────┘                   └─┘  └────────┘
pid                             └─┘  └────────┘
st   ──────────────────────────────────────────┘└─
499    let δ := min (ε/2/2 * ∥r∥^2) (∥r∥/2),
id              └─┘             
src    └───────┘└─┘   └┘ └─┘     └┘
typ    └───────┘└─┘  └┘ └─┘    └┘
doc    └───────┘       └┘     └─┘     └┘
txt    └───────┘       └┘     └─┘     └┘
par    └───────┘       └┘     └─┘     └┘
pid    └───┘└─┘       └┘     └─┘     └┘
st   ─────────────────────────────────────┘└─
500    have norm_r_pos : 0 < ∥r∥ := (norm_pos_iff r).mpr r0,
id                                 └──────────┘       └┘
src    └──────────────────┘   └──┘ └──────────┘ └────┘
typ    └──────────────────┘  └──┘ └──────────┘└────┘└┘
doc    └──────────────────┘    └──┘              └────┘
txt    └──────────────────┘    └──┘              └────┘
par    └──────────────────┘    └──┘              └────┘
pid    └─────────────┘└───┘    └──┘              └────┘
st   ─────────────────────────────────────────────────────┘└─
501    have A : 0 < ε / 2 / 2 * ∥r∥ ^ 2 := mul_pos' (half_pos (half_pos εpos)) (pow_pos norm_r_pos 2),
id                                       └──────┘            └──────┘ └──┘    └─────┘ └────────┘
src    └─────────┘   └─┘ └─┘     └────┘└──────┘          └──────┘    └─┘ └─────┘          └─┘
typ    └─────────┘  └─┘ └─┘    └────┘└──────┘          └──────┘└──┘└─┘ └─────┘└────────┘└─┘
doc    └─────────┘   └─┘ └─┘     └────┘                              └─┘                  └─┘
txt    └─────────┘   └─┘ └─┘     └────┘                              └─┘                  └─┘
par    └─────────┘   └─┘ └─┘     └────┘                              └─┘                  └─┘
pid    └────┘└───┘   └─┘ └─┘     └───┘                              └─┘                  └─┘
st   ───────────────────────────────────────────────────────────────────────────────────────────────┘└─
502    have δpos : 0 < δ, by simp [half_pos norm_r_pos, A],
id                                └──────┘ └────────┘  
src    └────────────┘       └────┘└──────┘          └┘ 
typ    └────────────┘      └────┘└──────┘└────────┘└┘
doc    └────────────┘       └────┘                  └┘ 
txt    └────────────┘       └────┘                  └┘ 
par    └────────────┘       └────┘                  └┘ 
pid    └───────┘└───┘                             └┘ 
st   ──────────────────┘                                  └─
503    refine ⟨ball r δ, ball_mem_nhds r δpos, λx hx, _⟩,
id             └──┘     └───────────┘  └──┘
src    └─────┘ └──┘  └┘└───────────┘     └┘ └──────┘
typ    └─────┘ └──┘ └┘└───────────┘└──┘└┘ └──────┘
doc    └─────┘ └──┘  └┘                  └┘ └──────┘
txt    └─────┘       └┘                  └┘ └──────┘
par    └─────┘       └┘                  └┘ └──────┘
pid                 └┘                  └┘ └──────┘
st   ──────────────────────────────────────────────────┘└─
504    have rx : ∥r∥/2 ≤ ∥x∥ := calc
id                      
src    └────────┘    └┘   └──┘    
typ    └────────┘   └┘  └──┘    
doc    └────────┘    └┘    └──┘    
txt    └────────┘    └┘    └──┘    
par    └────────┘    └┘    └──┘    
pid    └─────┘└─┘    └┘    └──┘    
st   ────────────────────────────────
505      ∥r∥/2 = ∥r∥ - ∥r∥/2 : by ring
src  ───┘    └┘         └──┘  └────
typ  ───┘    └┘         └──┘  └────
doc  ───┘    └┘         └──┘  └────
txt  ───┘    └┘         └──┘  └────
par  ───┘    └┘         └──┘  └────
pid  ───┘    └┘         └──┘  └─────
st   ───────────────────────────┘└─────
506      ... ≤ ∥r∥ - ∥r - x∥ :
src  ───┘└──┘          └──
typ  ───┘└──┘          └──
doc  ───┘└──┘          └──
txt  ───┘└──┘          └──
par  ───┘└──┘          └──
pid  ───────┘          └──
st   ───┘└─────────────────────
507      begin
src  ───┘     
typ  ───┘     
doc  ───┘     
txt  ───┘     
par  ───┘     
pid  ───┘     
st   ───┘└─────
508        apply sub_le_sub (le_refl _),
id               └────────┘  └─────┘
src  ─────┘└────┘└────────┘ └─────┘└─┘└─
typ  ─────┘└────┘└────────┘ └─────┘└─┘└─
doc  ─────┘└────┘                  └─┘└─
txt  ─────┘└────┘                  └─┘└─
par  ─────┘└────┘                  └─┘└─
pid  ───────────┘                  └────
st   ─────────────────────────────────┘└─
509        rw ← dist_eq_norm,
id              └──────────┘
src  ─────┘└───┘└──────────┘└─
typ  ─────┘└───┘└──────────┘└─
doc  ─────┘└───┘            └─
txt  ─────┘└───┘            └─
par  ─────┘└───┘            └─
pid  ──────────┘            └─
st   ──────────────────────┘└─
510        exact le_trans (le_of_lt (mem_ball'.1 hx)) (min_le_right _ _)
id               └──────┘  └──────┘  └───────┘   └┘    └──────────┘
src  ─────┘└────┘└──────┘ └──────┘ └───────┘└─┘  └─┘ └──────────┘└─────
typ  ─────┘└────┘└──────┘ └──────┘ └───────┘└─┘└┘└─┘ └──────────┘└─────
doc  ─────┘└────┘                           └─┘  └─┘             └─────
txt  ─────┘└────┘                           └─┘  └─┘             └─────
par  ─────┘└────┘                           └─┘  └─┘             └─────
pid  ───────────┘                           └─┘  └─┘             └─────
st   ────────────────────────────────────────────────────────────────────
511      end
src  ───┘└───
typ  ───┘└───
doc  ───┘└───
txt  ───┘└───
par  ───┘└───
pid  ────────
st   ───┘└─┘
512      ... ≤ ∥r - (r - x)∥ : norm_sub_norm_le r (r - x)
id                            └──────────────┘       
src  ───────┘        └─┘└──────────────┘     └─
typ  ───────┘        └─┘└──────────────┘   └─
doc  ───────┘         └─┘                     └─
txt  ───────┘         └─┘                     └─
par  ───────┘         └─┘                     └─
pid  ───────┘         └─┘                     └─
st   ─────────────────────────────────────────────────────
513      ... = ∥x∥ : by simp,
src  ───────┘    └─┘  └──┘
typ  ───────┘    └─┘  └──┘
doc  ───────┘    └─┘  └──┘
txt  ───────┘    └─┘  └──┘
par  ───────┘    └─┘  └──┘
pid  ───────┘    └─┘  └───┘
st   ─────────────────┘└───┘└─
514    have norm_x_pos : 0 < ∥x∥ := lt_of_lt_of_le (half_pos norm_r_pos) rx,
id                                 └────────────┘  └──────┘ └────────┘  └┘
src    └──────────────────┘    └──┘└────────────┘ └──────┘          └┘
typ    └──────────────────┘   └──┘└────────────┘ └──────┘└────────┘└┘└┘
doc    └──────────────────┘    └──┘                                 └┘
txt    └──────────────────┘    └──┘                                 └┘
par    └──────────────────┘    └──┘                                 └┘
pid    └─────────────┘└───┘    └──┘                                 └┘
st   ─────────────────────────────────────────────────────────────────────┘└─
515    have : x⁻¹ - r⁻¹ = (r - x) * x⁻¹ * r⁻¹,
id             └┘                       
src    └─────┘ └┘        └┘     
typ    └─────┘ └┘        └┘    
doc    └─────┘            └┘     
txt    └─────┘            └┘     
par    └─────┘            └┘     
pid    └───┘└┘            └┘     
st   ───────────────────────────────────────┘
516      by rw [sub_mul, sub_mul, mul_inv_cancel ((norm_pos_iff x).mp norm_x_pos), one_mul, mul_comm,
id              └─────┘  └─────┘  └────────────┘   └──────────┘      └────────┘   └─────┘  └──────┘
src         └──┘└─────┘└┘└─────┘└┘└────────────┘  └──────────┘ └───┘          └─┘└─────┘└┘└──────┘└─
typ         └──┘└─────┘└┘└─────┘└┘└────────────┘  └──────────┘└───┘└────────┘└─┘└─────┘└┘└──────┘└─
doc         └──┘       └┘       └┘                             └───┘          └─┘       └┘        └─
txt         └──┘       └┘       └┘                             └───┘          └─┘       └┘        └─
par         └──┘       └┘       └┘                             └───┘          └─┘       └┘        └─
pid           └┘       └┘       └┘                             └───┘          └─┘       └┘        └─
st              └─────┘└───────┘└───────────────────────────────────────────────┘└───────┘└────────┘└─
517             ← mul_assoc, inv_mul_cancel r0, one_mul],
id                └───────┘  └────────────┘ └┘  └─────┘
src  ────────────┘└───────┘└┘└────────────┘  └┘└─────┘
typ  ────────────┘└───────┘└┘└────────────┘└┘└┘└─────┘
doc  ────────────┘         └┘                └┘       
txt  ────────────┘         └┘                └┘       
par  ────────────┘         └┘                └┘       
pid  ────────────┘         └┘                └┘       
st   ─────────────────────┘└─────────────────┘└───────┘└─
518    calc dist x⁻¹ r⁻¹ = ∥x⁻¹ - r⁻¹∥ : dist_eq_norm _ _
id     └──┘ └──┘                       └──────────┘
src    └──┘ └──┘                         └──────────┘
typ    └──┘ └──┘                       └──────────┘
doc    └──┘
st   ─────────────────────────────────────────────────────
519    ... ≤ ∥r-x∥ * ∥x∥⁻¹ * ∥r∥⁻¹ : by rw [this, norm_mul, norm_mul, norm_inv, norm_inv]
id                                          └──┘  └──────┘  └──────┘  └──────┘  └──────┘
src                                     └──┘    └┘└──────┘└┘└──────┘└┘└──────┘└┘└──────┘└─
typ                                     └──┘└──┘└┘└──────┘└┘└──────┘└┘└──────┘└┘└──────┘└─
doc                                     └──┘    └┘        └┘        └┘        └┘        └─
txt                                     └──┘    └┘        └┘        └┘        └┘        └─
par                                     └──┘    └┘        └┘        └┘        └┘        └─
pid                                       └┘    └┘        └┘        └┘        └┘        
st   ─────────────────────────────────┘└───────┘└────────┘└────────┘└────────┘└────────┘
520    ... ≤ (ε/2/2 * ∥r∥^2) * (2 * ∥r∥⁻¹) * (∥r∥⁻¹) : begin
id            
src  ─┘
typ  ─┘       
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└──────────────────────────────────────────────┘└─────
521      apply_rules [mul_le_mul, inv_nonneg.2, le_of_lt A, norm_nonneg, inv_nonneg.2, mul_nonneg,
id                    └────────┘  └────────┘    └──────┘   └─────────┘  └────────┘    └────────┘
src      └───────────┘└────────┘└┘└────────┘└──┘└──────┘ └┘└─────────┘└┘└────────┘└──┘└────────┘└─
typ      └───────────┘└────────┘└┘└────────┘└──┘└──────┘└┘└─────────┘└┘└────────┘└──┘└────────┘└─
doc      └───────────┘          └┘          └──┘         └┘           └┘          └──┘          └─
txt      └───────────┘          └┘          └──┘         └┘           └┘          └──┘          └─
par      └───────────┘          └┘          └──┘         └┘           └┘          └──┘          └─
pid                 └┘          └┘          └──┘         └┘           └┘          └──┘          └─
st   ──────────────────────────────────────────────────────────────────────────────────────────────
522                   (inv_le_inv norm_x_pos norm_r_pos).2, le_refl],
id                     └────────┘ └────────┘ └────────┘     └─────┘
src  ────────────────┘ └────────┘                    └───┘└─────┘
typ  ────────────────┘ └────────┘└────────┘└────────┘└───┘└─────┘
doc  ────────────────┘                               └───┘       
txt  ────────────────┘                               └───┘       
par  ────────────────┘                               └───┘       
pid  ────────────────┘                               └───┘       
st   ──────────────────────────────────────────────────────────────┘└─
523      show ∥r - x∥ ≤ ε / 2 / 2 * ∥r∥ ^ 2,
id                                 
src      └───┘        └─┘ └─┘     └┘
typ      └───┘      └─┘ └─┘    └┘
doc      └───┘        └─┘ └─┘     └┘
txt      └───┘        └─┘ └─┘     └┘
par      └───┘        └─┘ └─┘     └┘
pid      └───┘        └─┘ └─┘     
st   ─────────────────────────────────────┘
524        by { rw ← dist_eq_norm, exact le_trans (le_of_lt (mem_ball'.1 hx)) (min_le_left _ _) },
id                   └──────────┘        └──────┘  └──────┘  └───────┘   └┘    └─────────┘
src             └───┘└──────────┘  └────┘└──────┘ └──────┘ └───────┘└─┘  └─┘ └─────────┘└────┘
typ             └───┘└──────────┘  └────┘└──────┘ └──────┘ └───────┘└─┘└┘└─┘ └─────────┘└────┘
doc             └───┘              └────┘                           └─┘  └─┘            └────┘
txt             └───┘              └────┘                           └─┘  └─┘            └────┘
par             └───┘              └────┘                           └─┘  └─┘            └────┘
pid               └─┘                                              └─┘  └─┘            └───┘
st            └────────────────┘└─────────────────────────────────────────────────────────────┘└┘
525      show ∥x∥⁻¹ ≤ 2 * ∥r∥⁻¹,
id                        
src      └───┘      └─┘ 
typ      └───┘     └─┘  
doc      └───┘      └─┘ 
txt      └───┘      └─┘ 
par      └───┘      └─┘ 
pid      └───┘      └─┘ 
st   ─────────────────────────┘└─
526      { convert (inv_le_inv norm_x_pos (half_pos norm_r_pos)).2 rx,
id                  └────────┘ └────────┘  └──────┘ └────────┘     └┘
src        └──────┘ └────────┘           └──────┘          └───┘
typ        └──────┘ └────────┘└────────┘ └──────┘└────────┘└───┘└┘
doc        └──────┘                                        └───┘
txt        └──────┘                                        └───┘
par        └──────┘                                        └───┘
pid                                                       └───┘
st   ─────┘└────────────────────────────────────────────────────────┘└─
527        rw [inv_div (ne.symm (ne_of_lt norm_r_pos)), div_eq_inv_mul, mul_comm],
id             └─────┘  └─────┘  └──────┘ └────────┘    └────────────┘  └──────┘
src        └──┘└─────┘ └─────┘ └──────┘          └──┘└────────────┘└┘└──────┘
typ        └──┘└─────┘ └─────┘ └──────┘└────────┘└──┘└────────────┘└┘└──────┘
doc        └──┘                                  └──┘              └┘        
txt        └──┘                                  └──┘              └┘        
par        └──┘                                  └──┘              └┘        
pid          └┘                                  └──┘              └┘        
st   ────────────────────────────────────────────────┘└──────────────┘└────────┘└──
528        norm_num },
src        └───────┘
typ        └───────┘
doc        └───────┘
txt        └───────┘
par        └───────┘
pid                
st   ──────────────┘└┘
529      show (0 : ℝ) ≤ 2, by norm_num
src      └───┘ └──┘ └┘ └┘     └────────
typ      └───┘ └──┘ └┘ └┘     └────────
doc      └───┘ └──┘ └┘ └┘     └────────
txt      └───┘ └──┘ └┘ └┘     └────────
par      └───┘ └──┘ └┘ └┘     └────────
pid      └───┘ └──┘ └┘              
st   ───────────────────┘
530    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st     └─┘
531    ... = ε/2 * (∥r∥ * ∥r∥⁻¹)^2 : by { generalize : ∥r∥⁻¹ = u, ring }
id                                                      
src                                       └───────────┘         └───┘
typ                                       └───────────┘        └───┘
doc                                       └───────────┘         └───┘
txt                                       └───────────┘         └───┘
par                                       └───────────┘         └───┘
pid                                                              
st   ─────────────────────────────────┘└───────────────────────┘└─────┘└┘
532    ... = ε/2 : by { rw [mul_inv_cancel (ne.symm (ne_of_lt norm_r_pos))], simp }
id                          └────────────┘  └─────┘  └──────┘ └────────┘
src                     └──┘└────────────┘ └─────┘ └──────┘          └─┘  └───┘
typ                     └──┘└────────────┘ └─────┘ └──────┘└────────┘└─┘  └───┘
doc                     └──┘                                         └─┘  └───┘
txt                     └──┘                                         └─┘  └───┘
par                     └──┘                                         └─┘  └───┘
pid                       └┘                                         └─┘      
st   └──────────────┘└───────────────────────────────────────────────────┘└──────┘└┘
533    ... < ε : half_lt_self εpos
id               └──────────┘ └──┘
src              └──────────┘
typ              └──────────┘ └──┘
st   └───────────────────────────┘
534  end
st   ──┘
535  
536  lemma continuous_on_inv [normed_field α] : continuous_on (λ(x:α), x⁻¹) {x | x ≠ 0} :=
id                            └──────────┘     └───────────┘         └┘      
src                           └──────────┘      └───────────┘           └┘        
typ                           └──────────┘     └───────────┘         └┘      
doc                           └──────────┘      └───────────┘
537  begin
st   └─────
538    assume x hx,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid    └─────────┘
st   ────────────┘└─
539    apply continuous_at.continuous_within_at,
id           └────────────────────────────────┘
src    └────┘└────────────────────────────────┘
typ    └────┘└────────────────────────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ─────────────────────────────────────────┘└─
540    exact (tendsto_inv hx)
id            └─────────┘ └┘
src    └────┘ └─────────┘  └┘
typ    └────┘ └─────────┘└┘└┘
doc    └────┘              └┘
txt    └────┘              └┘
par    └────┘              └┘
pid                       
st   ────────────────────────┘
541  end
st   └─┘
542  
543  instance : normed_field ℝ :=
id              └──────────┘ 
src             └──────────┘ 
typ             └──────────┘ 
doc             └──────────┘
544  { norm := λ x, abs x,
id                 └─┘ 
src                 └─┘
typ                └─┘ 
545    dist_eq := assume x y, rfl,
id                          └─┘
src                           └─┘
typ                         └─┘
546    norm_mul' := abs_mul }
id                  └─────┘
src                 └─────┘
typ                 └─────┘
547  
548  instance : nondiscrete_normed_field ℝ :=
id              └──────────────────────┘ 
src             └──────────────────────┘ 
typ             └──────────────────────┘ 
doc             └──────────────────────┘
549  { non_trivial := ⟨2, by { unfold norm, rw abs_of_nonneg; norm_num }⟩ }
id                                             └───────────┘
src                            └─────────┘  └─┘└───────────┘  └───────┘
typ                            └─────────┘  └─┘└───────────┘  └───────┘
doc                            └─────────┘  └─┘               └───────┘
txt                            └─────────┘  └─┘               └───────┘
par                            └─────────┘  └─┘               └───────┘
pid                                  └───┘                           
st                          └────────────┘└───────────────────────────┘└┘
550  end normed_field
551  
552  /-- If a function converges to a nonzero value, its inverse converges to the inverse of this value.
553  We use the name `tendsto.inv'` as `tendsto.inv` is already used in multiplicative topological
554  groups. -/
555  lemma filter.tendsto.inv' [normed_field α] {l : filter β} {f : β → α} {y : α}
id                              └──────────┘        └────┘                  
src                             └──────────┘         └────┘
typ                             └──────────┘        └────┘                  
doc                             └──────────┘
556    (hy : y ≠ 0) (h : tendsto f l (𝓝 y)) :
id                     └─────┘     
src                     └─────┘      
typ                    └─────┘     
doc                      └─────┘      
557    tendsto (λx, (f x)⁻¹) l (𝓝 y⁻¹) :=
id     └─────┘        └┘     └┘
src    └─────┘           └┘       └┘
typ    └─────┘        └┘     └┘
doc    └─────┘                  
558  (normed_field.tendsto_inv hy).comp h
id    └──────────────────────┘ └┘ └──┘  
src   └──────────────────────┘    └──┘
typ   └──────────────────────┘ └┘ └──┘  
559  
560  lemma filter.tendsto.div [normed_field α] {l : filter β} {f g : β → α} {x y : α}
id                             └──────────┘        └────┘                      
src                            └──────────┘         └────┘
typ                            └──────────┘        └────┘                      
doc                            └──────────┘
561    (hf : tendsto f l (𝓝 x)) (hg : tendsto g l (𝓝 y)) (hy : y ≠ 0) :
id           └─────┘              └─────┘               
src          └─────┘                 └─────┘                   
typ          └─────┘              └─────┘               
doc          └─────┘                 └─────┘      
562    tendsto (λa, f a / g a) l (𝓝 (x / y)) :=
id     └─────┘                 
src    └─────┘                       
typ    └─────┘                 
doc    └─────┘                    
563  hf.mul (hg.inv' hy)
id   └┘└──┘  └┘└───┘ └┘
src    └──┘    └───┘
typ  └┘└──┘  └┘└───┘ └┘
doc            └───┘
564  
565  lemma real.norm_eq_abs (r : ℝ) : norm r = abs r := rfl
id                                   └──┘   └─┘     └─┘
src                                  └──┘    └─┘      └─┘
typ                                  └──┘   └─┘     └─┘
566  
567  @[simp] lemma norm_norm [normed_group α] (x : α) : ∥∥x∥∥ = ∥x∥ :=
id                            └──────────┘            └┘└┘  
src                           └──────────┘              └┘ └┘   
typ                           └──────────┘              
doc    └──┘                   └──────────┘
568  by rw [real.norm_eq_abs, abs_of_nonneg (norm_nonneg _)]
id          └──────────────┘  └───────────┘  └─────────┘
src     └──┘└──────────────┘└┘└───────────┘ └─────────┘└────
typ     └──┘└──────────────┘└┘└───────────┘ └─────────┘└────
doc     └──┘                └┘                         └────
txt     └──┘                └┘                         └────
par     └──┘                └┘                         └────
pid       └┘                └┘                         └──┘
st     └───────────────────┘└─────────────────────────────┘
569  
src  
typ  
doc  
txt  
par  
pid  
st   
570  @[simp] lemma nnnorm_norm [normed_group α] (a : α) : nnnorm ∥a∥ = nnnorm a :=
id                              └──────────┘            └────┘   └────┘ 
src                             └──────────┘              └────┘    └────┘
typ                             └──────────┘            └────┘   └────┘ 
doc    └──┘                     └──────────┘              └────┘       └────┘
571  by simp only [nnnorm, norm_norm]
id                 └────┘  └───────┘
src     └─────────┘└────┘└┘└───────┘└─
typ     └─────────┘└────┘└┘└───────┘└─
doc     └─────────┘└────┘└┘         └─
txt     └─────────┘      └┘         └─
par     └─────────┘      └┘         └─
pid         └──┘└┘      └┘         
st     └──────────────────────────────
572  
src  
typ  
doc  
txt  
par  
pid  
st   
573  instance : normed_ring ℤ :=
id              └─────────┘ 
src             └─────────┘ 
typ             └─────────┘ 
doc             └─────────┘
574  { norm := λ n, ∥(n : ℝ)∥,
id                      
src                       
typ                     
575    norm_mul := λ m n, le_of_eq $ by simp only [norm, int.cast_mul, abs_mul],
id                      └──────┘                       └──────────┘  └─────┘
src                       └──────┘      └─────────┘    └┘└──────────┘└┘└─────┘
typ                     └──────┘      └─────────┘    └┘└──────────┘└┘└─────┘
doc                                     └─────────┘    └┘            └┘       
txt                                     └─────────┘    └┘            └┘       
par                                     └─────────┘    └┘            └┘       
pid                                         └──┘└┘    └┘            └┘       
st                                     └──────────────────────────────────────┘
576    dist_eq := λ m n, by simp only [int.dist_eq, norm, int.cast_sub] }
id                                   └─────────┘        └──────────┘
src                         └─────────┘└─────────┘└┘    └┘└──────────┘└┘
typ                       └─────────┘└─────────┘└┘    └┘└──────────┘└┘
doc                         └─────────┘           └┘    └┘            └┘
txt                         └─────────┘           └┘    └┘            └┘
par                         └─────────┘           └┘    └┘            └┘
pid                             └──┘└┘           └┘    └┘            
st                         └───────────────────────────────────────────┘
577  
578  @[elim_cast] lemma int.norm_cast_real (m : ℤ) : ∥(m : ℝ)∥ = ∥m∥ := rfl
id                                                             └─┘
src                                                              └─┘
typ                                                            └─┘
doc    └───────┘
579  
580  instance : normed_field ℚ :=
id              └──────────┘ 
src             └──────────┘ 
typ             └──────────┘ 
doc             └──────────┘ 
581  { norm := λ r, ∥(r : ℝ)∥,
id                      
src                       
typ                     
582    norm_mul' := λ r₁ r₂, by simp only [norm, rat.cast_mul, abs_mul],
id                    └┘ └┘                      └──────────┘  └─────┘
src                             └─────────┘    └┘└──────────┘└┘└─────┘
typ                   └┘ └┘     └─────────┘    └┘└──────────┘└┘└─────┘
doc                             └─────────┘    └┘            └┘       
txt                             └─────────┘    └┘            └┘       
par                             └─────────┘    └┘            └┘       
pid                                 └──┘└┘    └┘            └┘       
st                             └──────────────────────────────────────┘
583    dist_eq := λ r₁ r₂, by simp only [rat.dist_eq, norm, rat.cast_sub] }
id                  └┘ └┘                └─────────┘        └──────────┘
src                           └─────────┘└─────────┘└┘    └┘└──────────┘└┘
typ                 └┘ └┘     └─────────┘└─────────┘└┘    └┘└──────────┘└┘
doc                           └─────────┘           └┘    └┘            └┘
txt                           └─────────┘           └┘    └┘            └┘
par                           └─────────┘           └┘    └┘            └┘
pid                               └──┘└┘           └┘    └┘            
st                           └───────────────────────────────────────────┘
584  
585  instance : nondiscrete_normed_field ℚ :=
id              └──────────────────────┘ 
src             └──────────────────────┘ 
typ             └──────────────────────┘ 
doc             └──────────────────────┘ 
586  { non_trivial := ⟨2, by { unfold norm, rw abs_of_nonneg; norm_num }⟩ }
id                                             └───────────┘
src                            └─────────┘  └─┘└───────────┘  └───────┘
typ                            └─────────┘  └─┘└───────────┘  └───────┘
doc                            └─────────┘  └─┘               └───────┘
txt                            └─────────┘  └─┘               └───────┘
par                            └─────────┘  └─┘               └───────┘
pid                                  └───┘                           
st                          └────────────┘└───────────────────────────┘└┘
587  
588  @[elim_cast, simp] lemma rat.norm_cast_real (r : ℚ) : ∥(r : ℝ)∥ = ∥r∥ := rfl
id                                                                   └─┘
src                                                                    └─┘
typ                                                                  └─┘
doc    └───────┘  └──┘                                
589  
590  @[elim_cast, simp] lemma int.norm_cast_rat (m : ℤ) : ∥(m : ℚ)∥ = ∥m∥ :=
id                                                              
src                                                               
typ                                                             
doc    └───────┘  └──┘                                          
591  by rw [← rat.norm_cast_real, ← int.norm_cast_real]; congr' 1; norm_cast
id            └────────────────┘    └────────────────┘
src     └────┘└────────────────┘└──┘└────────────────┘  └──────┘  └─────────
typ     └────┘└────────────────┘└──┘└────────────────┘  └──────┘  └─────────
doc     └────┘                  └──┘                    └──────┘  └─────────
txt     └────┘                  └──┘                    └──────┘  └─────────
par     └────┘                  └──┘                    └──────┘  └─────────
pid       └──┘                  └──┘                                     
st     └───────────────────────┘└────────────────────┘└─────────────────────
592  
src  
typ  
doc  
txt  
par  
pid  
st   
593  section normed_space
594  
595  section prio
596  set_option default_priority 100 -- see Note [default priority]
doc             └──────────────┘
597  -- see Note[vector space definition] for why we extend `module`.
598  /-- A normed space over a normed field is a vector space endowed with a norm which satisfies the
599  equality `∥c • x∥ = ∥c∥ ∥x∥`. -/
600  class normed_space (α : Type*) (β : Type*) [normed_field α] [normed_group β]
id                           └───┘       └───┘   └──────────┘    └──────────┘ 
src                                              └──────────┘     └──────────┘
typ                          └───┘       └───┘   └──────────┘    └──────────┘ 
doc                                              └──────────┘     └──────────┘
601    extends module α β :=
id             └────┘  
src            └────┘
typ            └────┘  
doc            └────┘
602  (norm_smul : ∀ (a:α) (b:β), norm (a • b) = has_norm.norm a * norm b)
id                            └──┘       └───────────┘   └──┘ 
src                              └──┘         └───────────┘    └──┘
typ                           └──┘       └───────────┘   └──┘ 
603  end prio
604  
605  variables [normed_field α] [normed_group β]
id              └──────────┘     └──────────┘
src             └──────────┘     └──────────┘
typ             └──────────┘     └──────────┘
doc             └──────────┘     └──────────┘
606  
607  instance normed_field.to_normed_space : normed_space α α :=
id                                           └──────────┘  
src                                          └──────────┘
typ                                          └──────────┘  
doc                                          └──────────┘
608  { norm_smul := normed_field.norm_mul }
id                  └───────────────────┘
src                 └───────────────────┘
typ                 └───────────────────┘
609  
610  set_option class.instance_max_depth 43
doc             └──────────────────────┘
611  
612  lemma norm_smul [normed_space α β] (s : α) (x : β) : ∥s • x∥ = ∥s∥ * ∥x∥ :=
id                    └──────────┘                          
src                   └──────────┘                                  
typ                   └──────────┘                          
doc                   └──────────┘
613  normed_space.norm_smul s x
id   └────────────────────┘  
src  └────────────────────┘
typ  └────────────────────┘  
614  
615  lemma dist_smul [normed_space α β] (s : α) (x y : β) : dist (s • x) (s • y) = ∥s∥ * dist x y :=
id                    └──────────┘                      └──┘              └──┘  
src                   └──────────┘                          └──┘                   └──┘
typ                   └──────────┘                      └──┘              └──┘  
doc                   └──────────┘
616  by simp only [dist_eq_norm, (norm_smul _ _).symm, smul_sub]
id                 └──────────┘   └───────┘            └──────┘
src     └─────────┘└──────────┘└┘ └───────┘└──────────┘└──────┘└─
typ     └─────────┘└──────────┘└┘ └───────┘└──────────┘└──────┘└─
doc     └─────────┘            └┘          └──────────┘        └─
txt     └─────────┘            └┘          └──────────┘        └─
par     └─────────┘            └┘          └──────────┘        └─
pid         └──┘└┘            └┘          └──────────┘        
st     └─────────────────────────────────────────────────────────
617  
src  
typ  
doc  
txt  
par  
pid  
st   
618  lemma nnnorm_smul [normed_space α β] (s : α) (x : β) : nnnorm (s • x) = nnnorm s * nnnorm x :=
id                      └──────────┘                    └────┘       └────┘   └────┘ 
src                     └──────────┘                        └────┘         └────┘    └────┘
typ                     └──────────┘                    └────┘       └────┘   └────┘ 
doc                     └──────────┘                        └────┘           └────┘     └────┘
619  nnreal.eq $ norm_smul s x
id   └───────┘   └───────┘  
src  └───────┘   └───────┘
typ  └───────┘   └───────┘  
620  
621  variables {E : Type*} {F : Type*}
id                         
typ                        
622  [normed_group E] [normed_space α E] [normed_group F] [normed_space α F]
id    └──────────┘     └──────────┘       └──────────┘     └──────────┘
src   └──────────┘     └──────────┘       └──────────┘     └──────────┘
typ   └──────────┘     └──────────┘       └──────────┘     └──────────┘
doc   └──────────┘     └──────────┘       └──────────┘     └──────────┘
623  
624  lemma tendsto_smul {f : γ → α} { g : γ → F} {e : filter γ} {s : α} {b : F} :
id                                                └────┘               
src                                                   └────┘
typ                                               └────┘               
625    (tendsto f e (𝓝 s)) → (tendsto g e (𝓝 b)) → tendsto (λ x, (f x) • (g x)) e (𝓝 (s • b)) :=
id      └─────┘           └─────┘          └─────┘                      
src     └─────┘              └─────┘             └─────┘                            
typ     └─────┘           └─────┘          └─────┘                      
doc     └─────┘              └─────┘             └─────┘                         
626  begin
st   └─────
627    intros limf limg,
src    └──────────────┘
typ    └──────────────┘
doc    └──────────────┘
txt    └──────────────┘
par    └──────────────┘
pid          └────────┘
st   ─────────────────┘└─
628    rw tendsto_iff_norm_tendsto_zero,
id        └───────────────────────────┘
src    └─┘└───────────────────────────┘
typ    └─┘└───────────────────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ─────────────────────────────────┘└─
629    have ineq := λ x : γ, calc
id                        
src    └───────────┘ └───┘ └┘    
typ    └───────────┘ └───┘└┘    
doc    └───────────┘ └───┘ └┘    
txt    └───────────┘ └───┘ └┘    
par    └───────────┘ └───┘ └┘    
pid    └───────┘└─┘ └───┘ └┘    
st   ─────────────────────────────
630        ∥f x • g x - s • b∥ = ∥(f x • g x - s • g x) + (s • g x - s • b)∥ : by simp[add_assoc]
id                                                                                 └───────┘
src  ─────┘                    └┘           └─┘  └───┘└───────┘└─
typ  ─────┘                    └┘           └─┘  └───┘└───────┘└─
doc  ─────┘                        └┘           └─┘  └───┘         └─
txt  ─────┘                        └┘           └─┘  └───┘         └─
par  ─────┘                        └┘           └─┘  └───┘         └─
pid  ─────┘                        └┘           └─┘  └────┘         └─
st   ───────────────────────────────────────────────────────────────────────────┘└────────────────
631                        ... ≤ ∥f x • g x - s • g x∥ + ∥s • g x - s • b∥ : norm_add_le (f x • g x - s • g x) (s • g x - s • b)
id                                                                          └─────────┘                                   
src  ─────────────────────┘└──┘                       └─┘└─────────┘           └┘         └─
typ  ─────────────────────┘└──┘                       └─┘└─────────┘          └┘      └─
doc  ─────────────────────┘└──┘                        └─┘└─────────┘           └┘         └─
txt  ─────────────────────┘└──┘                        └─┘                      └┘         └─
par  ─────────────────────┘└──┘                        └─┘                      └┘         └─
pid  ─────────────────────────┘                        └─┘                      └┘         └─
st   ─────────────────────┘└─────────────────────────────────────────────────────────────────────────────────────────────────────
632                        ... ≤ ∥f x - s∥*∥g x∥ + ∥s∥*∥g x - b∥ : by { rw [←smul_sub, ←sub_smul, norm_smul, norm_smul] },
id                                                                          └──────┘   └──────┘  └───────┘  └───────┘
src  ─────────────────────────┘                      └─┘  └─┘└───┘└──────┘└─┘└──────┘└┘└───────┘└┘└───────┘└┘
typ  ─────────────────────────┘                      └─┘  └─┘└───┘└──────┘└─┘└──────┘└┘└───────┘└┘└───────┘└┘
doc  ─────────────────────────┘                       └─┘  └─┘└───┘        └─┘        └┘         └┘         └┘
txt  ─────────────────────────┘                       └─┘  └─┘└───┘        └─┘        └┘         └┘         └┘
par  ─────────────────────────┘                       └─┘  └─┘└───┘        └─┘        └┘         └┘         └┘
pid  ─────────────────────────┘                       └─┘  └──────┘        └─┘        └┘         └┘         └─┘
st   ───────────────────────────────────────────────────────────────┘└──────────────┘└─────────┘└─────────┘└─────────┘└┘
633    apply squeeze_zero,
id           └──────────┘
src    └────┘└──────────┘
typ    └────┘└──────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ───────────────────┘└─
634    { intro t, exact norm_nonneg _ },
id                      └─────────┘
src      └─────┘  └────┘└─────────┘└─┘
typ      └─────┘  └────┘└─────────┘└─┘
doc      └─────┘  └────┘           └─┘
txt      └─────┘  └────┘           └─┘
par      └─────┘  └────┘           └─┘
pid           └┘                  └┘
st   ───┘└─────┘└────────────────────┘└┘
635    { exact ineq },
id             └──┘
src      └────┘    
typ      └────┘└──┘
doc      └────┘    
txt      └────┘    
par      └────┘    
pid               
st   ───┘└─────────┘└┘
636    { clear ineq,
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid           └───┘
st   ─────────────┘└─
637  
st   
638      have limf': tendsto (λ x, ∥f x - s∥) e (𝓝 0) := tendsto_iff_norm_tendsto_zero.1 limf,
id                   └─────┘                         └───────────────────────────┘   └──┘
src      └──────────┘└─────┘  └──┘      └┘  └─────┘└───────────────────────────┘└─┘
typ      └──────────┘└─────┘  └──┘    └┘ └─────┘└───────────────────────────┘└─┘└──┘
doc      └──────────┘└─────┘  └──┘      └┘  └─────┘                             └─┘
txt      └──────────┘         └──┘      └┘   └─────┘                             └─┘
par      └──────────┘         └──┘      └┘   └─────┘                             └─┘
pid      └────────┘└┘         └──┘      └┘   └─┘└──┘                             └─┘
st   ───────────────────────────────────────────────────────────────────────────────────────┘└─
639      have limg' : tendsto (λ x, ∥g x∥) e (𝓝 ∥b∥) := filter.tendsto.comp (continuous_iff_continuous_at.1 continuous_norm _) limg,
id                    └─────┘                        └─────────────────┘  └──────────────────────────┘   └─────────────┘    └──┘
src      └───────────┘└─────┘  └──┘    └┘      └───┘└─────────────────┘ └──────────────────────────┘└─┘└─────────────┘└──┘
typ      └───────────┘└─────┘  └──┘   └┘    └───┘└─────────────────┘ └──────────────────────────┘└─┘└─────────────┘└──┘└──┘
doc      └───────────┘└─────┘  └──┘    └┘      └───┘                                                └─┘               └──┘
txt      └───────────┘         └──┘    └┘      └───┘                                                └─┘               └──┘
par      └───────────┘         └──┘    └┘      └───┘                                                └─┘               └──┘
pid      └────────┘└─┘         └──┘    └┘      └──┘                                                └─┘               └──┘
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
640  
st   
641      have lim1 := limf'.mul limg',
id                    └───────┘ └───┘
src      └───────────┘└───────┘
typ      └───────────┘└───────┘└───┘
doc      └───────────┘         
txt      └───────────┘         
par      └───────────┘         
pid      └───────┘└─┘         
st   ───────────────────────────────┘└─
642      simp only [zero_mul, sub_eq_add_neg] at lim1,
id                  └──────┘  └────────────┘
src      └─────────┘└──────┘└┘└────────────┘└───────┘
typ      └─────────┘└──────┘└┘└────────────┘└───────┘
doc      └─────────┘        └┘              └───────┘
txt      └─────────┘        └┘              └───────┘
par      └─────────┘        └┘              └───────┘
pid          └──┘└┘        └┘              └─────┘
st   ───────────────────────────────────────────────┘└─
643  
st   
644      have limg3 := tendsto_iff_norm_tendsto_zero.1 limg,
id                     └───────────────────────────┘   └──┘
src      └────────────┘└───────────────────────────┘└─┘
typ      └────────────┘└───────────────────────────┘└─┘└──┘
doc      └────────────┘                             └─┘
txt      └────────────┘                             └─┘
par      └────────────┘                             └─┘
pid      └────────┘└─┘                             └─┘
st   ─────────────────────────────────────────────────────┘└─
645  
st   
646      have lim2 := (tendsto_const_nhds : tendsto _ _ (𝓝 ∥ s ∥)).mul limg3,
id                     └────────────────┘   └─────┘                   └───┘
src      └───────────┘ └────────────────┘└─┘└─────┘└───┘     └─────┘
typ      └───────────┘ └────────────────┘└─┘└─────┘└───┘    └─────┘└───┘
doc      └───────────┘                   └─┘└─────┘└───┘     └─────┘
txt      └───────────┘                   └─┘       └───┘     └─────┘
par      └───────────┘                   └─┘       └───┘     └─────┘
pid      └───────┘└─┘                   └─┘       └───┘     └─────┘
st   ──────────────────────────────────────────────────────────────────────┘└─
647      simp only [sub_eq_add_neg, mul_zero] at lim2,
id                  └────────────┘  └──────┘
src      └─────────┘└────────────┘└┘└──────┘└───────┘
typ      └─────────┘└────────────┘└┘└──────┘└───────┘
doc      └─────────┘              └┘        └───────┘
txt      └─────────┘              └┘        └───────┘
par      └─────────┘              └┘        └───────┘
pid          └──┘└┘              └┘        └─────┘
st   ───────────────────────────────────────────────┘└─
648  
st   
649      rw [show (0:ℝ) = 0 + 0, by simp],
id                      
src      └──┘     └┘ └┘└─┘ └─────┘└──┘
typ      └──┘     └┘ └┘└─┘ └─────┘└──┘
doc      └──┘     └┘ └┘ └─┘ └─────┘└──┘
txt      └──┘     └┘ └┘ └─┘ └─────┘└──┘
par      └──┘     └┘ └┘ └─┘ └─────┘└──┘
pid        └┘     └┘ └┘ └─┘ └──────────┘
st   ─────────────────────────────┘└───┘└──
650      exact lim1.add lim2  }
id             └──────┘ └──┘
src      └────┘└──────┘    └┘
typ      └────┘└──────┘└──┘└┘
doc      └────┘            └┘
txt      └────┘            └┘
par      └────┘            └┘
pid                       └┘
st   ────────────────────────┘└─
651  end
st   ──┘
652  
653  lemma tendsto_smul_const {g : γ → F} {e : filter γ} (s : α) {b : F} :
id                                           └────┘               
src                                            └────┘
typ                                          └────┘               
654    (tendsto g e (𝓝 b)) → tendsto (λ x, s • (g x)) e (𝓝 (s • b)) :=
id      └─────┘          └─────┘                   
src     └─────┘             └─────┘                        
typ     └─────┘          └─────┘                   
doc     └─────┘             └─────┘                     
655  tendsto_smul tendsto_const_nhds
id   └──────────┘ └────────────────┘
src  └──────────┘ └────────────────┘
typ  └──────────┘ └────────────────┘
656  
657  @[priority 100] -- see Note [lower instance priority]
658  instance normed_space.topological_vector_space : topological_vector_space α E :=
id                                                    └──────────────────────┘  
src                                                   └──────────────────────┘
typ                                                   └──────────────────────┘  
doc                                                   └──────────────────────┘
659  { continuous_smul := continuous_iff_continuous_at.2 $ λp, tendsto_smul
id                        └──────────────────────────┘       └──────────┘
src                       └──────────────────────────┘        └──────────┘
typ                       └──────────────────────────┘       └──────────┘
660      (continuous_iff_continuous_at.1 continuous_fst _) (continuous_iff_continuous_at.1 continuous_snd _) }
id        └──────────────────────────┘  └────────────┘     └──────────────────────────┘  └────────────┘
src       └──────────────────────────┘  └────────────┘     └──────────────────────────┘  └────────────┘
typ       └──────────────────────────┘  └────────────┘     └──────────────────────────┘  └────────────┘
661  
662  open normed_field
663  
664  /-- If there is a scalar `c` with `∥c∥>1`, then any element can be moved by scalar multiplication to
665  any shell of width `∥c∥`. Also recap information on the norm of the rescaling element that shows
666  up in applications. -/
667  lemma rescale_to_shell {c : α} (hc : 1 < ∥c∥) {ε : ℝ} (εpos : 0 < ε) {x : E} (hx : x ≠ 0) :
id                                                                              
src                                                                                  
typ                                                                             
668    ∃d:α, d ≠ 0 ∧ ∥d • x∥ ≤ ε ∧ (ε/∥c∥ ≤ ∥d • x∥) ∧ (∥d∥⁻¹ ≤ ε⁻¹ * ∥c∥ * ∥x∥) :=
id                            └┘  └┘    
src                                     └┘   └┘      
typ                           └┘  └┘    
669  begin
st   └─────
670    have xεpos : 0 < ∥x∥/ε := div_pos_of_pos_of_pos ((norm_pos_iff _).2 hx) εpos,
id                         └───────────────────┘   └──────────┘      └┘  └──┘
src    └─────────────┘  └──┘└───────────────────┘  └──────────┘└────┘  └┘
typ    └─────────────┘└──┘└───────────────────┘  └──────────┘└────┘└┘└┘└──┘
doc    └─────────────┘      └──┘                                   └────┘  └┘
txt    └─────────────┘      └──┘                                   └────┘  └┘
par    └─────────────┘      └──┘                                   └────┘  └┘
pid    └────────┘└───┘      └──┘                                   └────┘  └┘
st   ─────────────────────────────────────────────────────────────────────────────┘└─
671    rcases exists_int_pow_near xεpos hc with ⟨n, hn⟩,
id            └─────────────────┘ └───┘ └┘
src    └─────┘└─────────────────┘       └───────────┘
typ    └─────┘└─────────────────┘└───┘└┘└───────────┘
doc    └─────┘└─────────────────┘       └───────────┘
txt    └─────┘                          └───────────┘
par    └─────┘                          └───────────┘
pid                                    └───────────┘
st   ─────────────────────────────────────────────────┘└─
672    have cpos : 0 < ∥c∥ := lt_trans (zero_lt_one : (0 :ℝ) < 1) hc,
id                           └──────┘  └─────────┘               └┘
src    └────────────┘    └──┘└──────┘ └─────────┘└─┘ └─┘ └┘ └──┘
typ    └────────────┘   └──┘└──────┘ └─────────┘└─┘ └─┘ └┘ └──┘└┘
doc    └────────────┘    └──┘                    └─┘ └─┘ └┘ └──┘
txt    └────────────┘    └──┘                    └─┘ └─┘ └┘ └──┘
par    └────────────┘    └──┘                    └─┘ └─┘ └┘ └──┘
pid    └───────┘└───┘    └──┘                    └─┘ └─┘ └┘ └──┘
st   ──────────────────────────────────────────────────────────────┘└─
673    have cnpos : 0 < ∥c^(n+1)∥ := by { rw norm_fpow, exact lt_trans xεpos hn.2 },
id                                       └───────┘        └──────┘ └───┘ └┘
src    └─────────────┘     └┘ └──┘  └─┘└─┘└───────┘└┘└────┘└──────┘       └─┘
typ    └─────────────┘   └┘ └──┘  └─┘└─┘└───────┘└┘└────┘└──────┘└───┘└┘└─┘
doc    └─────────────┘       └┘ └──┘  └─┘└─┘         └┘└────┘               └─┘
txt    └─────────────┘       └┘ └──┘  └─┘└─┘         └┘└────┘               └─┘
par    └─────────────┘       └┘ └──┘  └─┘└─┘         └┘└────┘               └─┘
pid    └────────┘└───┘       └┘ └──┘  └────┘         └──────┘               └──┘
st   ─────────────────────────────────┘└─────────────┘└──────────────────────────┘└┘
674    refine ⟨(c^(n+1))⁻¹, _, _, _, _⟩,
id                    └┘
src    └─────┘       └─┘└┘└───────────┘
typ    └─────┘     └─┘└┘└───────────┘
doc    └─────┘       └─┘  └───────────┘
txt    └─────┘       └─┘  └───────────┘
par    └─────┘       └─┘  └───────────┘
pid                 └─┘  └───────────┘
st   ─────────────────────────────────┘└─
675    show (c ^ (n + 1))⁻¹  ≠ 0,
id                         
src    └───┘      └──┘  └┘└┘
typ    └───┘    └──┘  └┘└┘
doc    └───┘      └──┘  └┘ └┘
txt    └───┘      └──┘  └┘ └┘
par    └───┘      └──┘  └┘ └┘
pid    └───┘      └──┘  └┘ 
st   ──────────────────────────┘
676      by rwa [ne.def, inv_eq_zero, ← ne.def, ← norm_pos_iff],
id               └────┘  └─────────┘    └────┘    └──────────┘
src         └───┘└────┘└┘└─────────┘└──┘└────┘└──┘└──────────┘
typ         └───┘└────┘└┘└─────────┘└──┘└────┘└──┘└──────────┘
doc         └───┘      └┘           └──┘      └──┘            
txt         └───┘      └┘           └──┘      └──┘            
par         └───┘      └┘           └──┘      └──┘            
pid            └┘      └┘           └──┘      └──┘            
st               └────┘└───────────┘└────────┘└──────────────┘└─
677    show ∥(c ^ (n + 1))⁻¹ • x∥ ≤ ε,
id                             
src    └───┘       └──┘    
typ    └───┘     └──┘   
doc    └───┘       └──┘      
txt    └───┘       └──┘      
par    └───┘       └──┘      
pid    └───┘       └──┘      
st   ──────────────────────────────────
678    { rw [norm_smul, norm_inv, ← div_eq_inv_mul, div_le_iff cnpos, mul_comm, norm_fpow],
id           └───────┘  └──────┘    └────────────┘  └────────┘ └───┘  └──────┘  └───────┘
src      └──┘└───────┘└┘└──────┘└──┘└────────────┘└┘└────────┘     └┘└──────┘└┘└───────┘
typ      └──┘└───────┘└┘└──────┘└──┘└────────────┘└┘└────────┘└───┘└┘└──────┘└┘└───────┘
doc      └──┘         └┘        └──┘              └┘               └┘        └┘         
txt      └──┘         └┘        └──┘              └┘               └┘        └┘         
par      └──┘         └┘        └──┘              └┘               └┘        └┘         
pid        └┘         └┘        └──┘              └┘               └┘        └┘         
st   ───┘└───────────┘└────────┘└────────────────┘└────────────────┘└────────┘└─────────┘└──
679      exact (div_le_iff εpos).1 (le_of_lt (hn.2)) },
id              └────────┘ └──┘     └──────┘  └┘
src      └────┘ └────────┘    └──┘ └──────┘   └───┘
typ      └────┘ └────────┘└──┘└──┘ └──────┘ └┘└───┘
doc      └────┘               └──┘            └───┘
txt      └────┘               └──┘            └───┘
par      └────┘               └──┘            └───┘
pid                          └──┘            └──┘
st   ───────────────────────────────────────────────┘└┘
680    show ε / ∥c∥ ≤ ∥(c ^ (n + 1))⁻¹ • x∥,
id                                    
src    └───┘             └──┘   
typ    └───┘          └──┘   
doc    └───┘             └──┘   
txt    └───┘             └──┘   
par    └───┘             └──┘   
pid    └───┘             └──┘   
st   ────────────────────────────────────────
681    { rw [div_le_iff cpos, norm_smul, norm_inv, norm_fpow, fpow_add (ne_of_gt cpos),
id           └────────┘ └──┘  └───────┘  └──────┘  └───────┘  └──────┘  └──────┘ └──┘
src      └──┘└────────┘    └┘└───────┘└┘└──────┘└┘└───────┘└┘└──────┘ └──────┘    └──
typ      └──┘└────────┘└──┘└┘└───────┘└┘└──────┘└┘└───────┘└┘└──────┘ └──────┘└──┘└──
doc      └──┘              └┘         └┘        └┘         └┘                     └──
txt      └──┘              └┘         └┘        └┘         └┘                     └──
par      └──┘              └┘         └┘        └┘         └┘                     └──
pid        └┘              └┘         └┘        └┘         └┘                     └──
st   ───┘└─────────────────┘└─────────┘└────────┘└─────────┘└────────────────────────┘└─
682          fpow_one, mul_inv', mul_comm, ← mul_assoc, ← mul_assoc, mul_inv_cancel (ne_of_gt cpos),
id           └──────┘  └──────┘  └──────┘    └───────┘    └───────┘  └────────────┘  └──────┘ └──┘
src  ───────┘└──────┘└┘└──────┘└┘└──────┘└──┘└───────┘└──┘└───────┘└┘└────────────┘ └──────┘    └──
typ  ───────┘└──────┘└┘└──────┘└┘└──────┘└──┘└───────┘└──┘└───────┘└┘└────────────┘ └──────┘└──┘└──
doc  ───────┘        └┘        └┘        └──┘         └──┘         └┘                           └──
txt  ───────┘        └┘        └┘        └──┘         └──┘         └┘                           └──
par  ───────┘        └┘        └┘        └──┘         └──┘         └┘                           └──
pid  ───────┘        └┘        └┘        └──┘         └──┘         └┘                           └──
st   ───────────────┘└────────┘└────────┘└───────────┘└───────────┘└──────────────────────────────┘└─
683          one_mul, ← div_eq_inv_mul, le_div_iff (fpow_pos_of_pos cpos _), mul_comm],
id           └─────┘    └────────────┘  └────────┘  └─────────────┘ └──┘     └──────┘
src  ───────┘└─────┘└──┘└────────────┘└┘└────────┘ └─────────────┘    └───┘└──────┘
typ  ───────┘└─────┘└──┘└────────────┘└┘└────────┘ └─────────────┘└──┘└───┘└──────┘
doc  ───────┘       └──┘              └┘                              └───┘        
txt  ───────┘       └──┘              └┘                              └───┘        
par  ───────┘       └──┘              └┘                              └───┘        
pid  ───────┘       └──┘              └┘                              └───┘        
st   ──────────────┘└────────────────┘└───────────────────────────────────┘└────────┘└──
684      exact (le_div_iff εpos).1 hn.1 },
id              └────────┘ └──┘    └┘
src      └────┘ └────────┘    └──┘  └─┘
typ      └────┘ └────────┘└──┘└──┘└┘└─┘
doc      └────┘               └──┘  └─┘
txt      └────┘               └──┘  └─┘
par      └────┘               └──┘  └─┘
pid                          └──┘  └─┘
st   ──────────────────────────────────┘└┘
685    show ∥(c ^ (n + 1))⁻¹∥⁻¹ ≤ ε⁻¹ * ∥c∥ * ∥x∥,
id                                         
src    └───┘       └──┘             
typ    └───┘      └──┘            
doc    └───┘       └──┘              
txt    └───┘       └──┘              
par    └───┘       └──┘              
pid    └───┘       └──┘              
st   ──────────────────────────────────────────────
686    { have : ε⁻¹ * ∥c∥ * ∥x∥ = ε⁻¹ * ∥x∥ * ∥c∥, by ring,
id                                          
src      └─────┘                           └──┘
typ      └─────┘                        └──┘
doc      └─────┘                            └──┘
txt      └─────┘                            └──┘
par      └─────┘                            └──┘
pid      └───┘└┘                    
st   ───────────────────────────────────────────┘         └─
687      rw [norm_inv, inv_inv', norm_fpow, fpow_add (ne_of_gt cpos), fpow_one, this, ← div_eq_inv_mul],
id           └──────┘  └──────┘  └───────┘  └──────┘  └──────┘ └──┘   └──────┘  └──┘    └────────────┘
src      └──┘└──────┘└┘└──────┘└┘└───────┘└┘└──────┘ └──────┘    └─┘└──────┘└┘    └──┘└────────────┘
typ      └──┘└──────┘└┘└──────┘└┘└───────┘└┘└──────┘ └──────┘└──┘└─┘└──────┘└┘└──┘└──┘└────────────┘
doc      └──┘        └┘        └┘         └┘                     └─┘        └┘    └──┘              
txt      └──┘        └┘        └┘         └┘                     └─┘        └┘    └──┘              
par      └──┘        └┘        └┘         └┘                     └─┘        └┘    └──┘              
pid        └┘        └┘        └┘         └┘                     └─┘        └┘    └──┘              
st   ───────────────┘└────────┘└─────────┘└────────────────────────┘└────────┘└────┘└────────────────┘└──
688      exact mul_le_mul_of_nonneg_right hn.1 (norm_nonneg _) }
id             └────────────────────────┘ └┘    └─────────┘
src      └────┘└────────────────────────┘  └─┘ └─────────┘└──┘
typ      └────┘└────────────────────────┘└┘└─┘ └─────────┘└──┘
doc      └────┘                            └─┘            └──┘
txt      └────┘                            └─┘            └──┘
par      └────┘                            └─┘            └──┘
pid                                       └─┘            └─┘
st   ─────────────────────────────────────────────────────────┘└─
689  end
st   ──┘
690  
691  /-- The product of two normed spaces is a normed space, with the sup norm. -/
692  instance : normed_space α (E × F) :=
id              └──────────┘     
src             └──────────┘      
typ             └──────────┘     
doc             └──────────┘
693  { norm_smul :=
694    begin
st     └─────
695      intros s x,
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid            └──┘
st   ─────────────┘└─
696      cases x with x₁ x₂,
id             
src      └────┘ └─────────┘
typ      └────┘└─────────┘
doc      └────┘ └─────────┘
txt      └────┘ └─────────┘
par      └────┘ └─────────┘
pid            └─────────┘
st   ─────────────────────┘└─
697      change max (∥s • x₁∥) (∥s • x₂∥) = ∥s∥ * max (∥x₁∥) (∥x₂∥),
id                                          └─┘   └┘     └┘
src      └─────┘       └┘       └┘   └─┘     └┘     
typ      └─────┘       └┘       └┘  └─┘  └┘ └┘  └┘ 
doc      └─────┘          └┘       └┘             └┘     
txt      └─────┘          └┘       └┘             └┘     
par      └─────┘          └┘       └┘             └┘     
pid                      └┘       └┘             └┘     
st   ─────────────────────────────────────────────────────────────┘└─
698      rw [norm_smul, norm_smul, ← mul_max_of_nonneg _ _ (norm_nonneg _)]
id           └───────┘  └───────┘    └───────────────┘      └─────────┘
src      └──┘└───────┘└┘└───────┘└──┘└───────────────┘└───┘ └─────────┘└────
typ      └──┘└───────┘└┘└───────┘└──┘└───────────────┘└───┘ └─────────┘└────
doc      └──┘         └┘         └──┘                 └───┘            └────
txt      └──┘         └┘         └──┘                 └───┘            └────
par      └──┘         └┘         └──┘                 └───┘            └────
pid        └┘         └┘         └──┘                 └───┘            └──┘
st   ────────────────┘└─────────┘└───────────────────────────────────────┘
699    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
700  
701    add_smul := λ r x y, prod.ext (add_smul _ _ _) (add_smul _ _ _),
id                       └──────┘  └──────┘         └──────┘
src                         └──────┘  └──────┘         └──────┘
typ                      └──────┘  └──────┘         └──────┘
702    smul_add := λ r x y, prod.ext (smul_add _ _ _) (smul_add _ _ _),
id                       └──────┘  └──────┘         └──────┘
src                         └──────┘  └──────┘         └──────┘
typ                      └──────┘  └──────┘         └──────┘
703    ..prod.normed_group,
id       └───────────────┘
src      └───────────────┘
typ      └───────────────┘
doc      └───────────────┘
704    ..prod.module }
id       └─────────┘
src      └─────────┘
typ      └─────────┘
705  
706  /-- The product of finitely many normed spaces is a normed space, with the sup norm. -/
707  instance pi.normed_space {E : ι → Type*} [fintype ι] [∀i, normed_group (E i)]
id                                            └─────┘       └──────────┘   
src                                            └─────┘         └──────────┘
typ                                           └─────┘       └──────────┘   
doc                                            └─────┘         └──────────┘
708    [∀i, normed_space α (E i)] : normed_space α (Πi, E i) :=
id         └──────────┘         └──────────┘       
src         └──────────┘            └──────────┘
typ        └──────────┘         └──────────┘       
doc         └──────────┘            └──────────┘
709  { norm_smul := λ a f,
id                     
typ                    
710      show (↑(finset.sup finset.univ (λ (b : ι), nnnorm (a • f b))) : ℝ) =
id              └────────┘ └─────────┘            └────┘             
src             └────────┘ └─────────┘             └────┘                
typ             └────────┘ └─────────┘            └────┘             
doc              └────────┘ └─────────┘             └────┘
711        nnnorm a * ↑(finset.sup finset.univ (λ (b : ι), nnnorm (f b))),
id         └────┘    └────────┘ └─────────┘            └────┘   
src        └────┘     └────────┘ └─────────┘             └────┘
typ        └────┘    └────────┘ └─────────┘            └────┘   
doc        └────┘       └────────┘ └─────────┘             └────┘
712      by simp only [(nnreal.coe_mul _ _).symm, nnreal.mul_finset_sup, nnnorm_smul] }
id                      └────────────┘            └───────────────────┘  └─────────┘
src         └─────────┘ └────────────┘└──────────┘└───────────────────┘└┘└─────────┘└┘
typ         └─────────┘ └────────────┘└──────────┘└───────────────────┘└┘└─────────┘└┘
doc         └─────────┘               └──────────┘                     └┘           └┘
txt         └─────────┘               └──────────┘                     └┘           └┘
par         └─────────┘               └──────────┘                     └┘           └┘
pid             └──┘└┘               └──────────┘                     └┘           
st         └─────────────────────────────────────────────────────────────────────────┘
713  
714  /-- A subspace of a normed space is also a normed space, with the restriction of the norm. -/
715  instance submodule.normed_space {𝕜 : Type*} [normed_field 𝕜]
id                                                └──────────┘ 
src                                               └──────────┘
typ                                               └──────────┘ 
doc                                               └──────────┘
716    {E : Type*} [normed_group E] [normed_space 𝕜 E] (s : submodule 𝕜 E) : normed_space 𝕜 s :=
id                  └──────────┘    └──────────┘         └───────┘      └──────────┘  
src                 └──────────┘     └──────────┘           └───────┘        └──────────┘
typ                 └──────────┘    └──────────┘         └───────┘      └──────────┘  
doc                 └──────────┘     └──────────┘           └───────┘        └──────────┘
717  { norm_smul := λc x, norm_smul c (x : E) }
id                      └───────┘      
src                       └───────┘
typ                     └───────┘      
718  
719  end normed_space
720  
721  section normed_algebra
722  
723  /-- A normed algebra `𝕜'` over `𝕜` is an algebra endowed with a norm for which the embedding of
724  `𝕜` in `𝕜'` is an isometry. -/
725  class normed_algebra (𝕜 : Type*) (𝕜' : Type*) [normed_field 𝕜] [normed_ring 𝕜']
id                             └───┘        └───┘   └──────────┘    └─────────┘ └┘
src                                                 └──────────┘     └─────────┘
typ                            └───┘        └───┘   └──────────┘    └─────────┘ └┘
doc                                                 └──────────┘     └─────────┘
726    extends algebra 𝕜 𝕜' :=
id             └─────┘  └┘
src            └─────┘
typ            └─────┘  └┘
doc            └─────┘
727  (norm_algebra_map_eq : ∀x:𝕜, ∥algebra_map 𝕜' x∥ = ∥x∥)
id                              └─────────┘ └┘   
src                               └─────────┘        
typ                             └─────────┘ └┘   
728  
729  @[simp] lemma norm_algebra_map_eq {𝕜 : Type*} (𝕜' : Type*) [normed_field 𝕜] [normed_ring 𝕜']
id                                                               └──────────┘    └─────────┘ └┘
src                                                              └──────────┘     └─────────┘
typ                                                              └──────────┘    └─────────┘ └┘
doc    └──┘                                                      └──────────┘     └─────────┘
730    [h : normed_algebra 𝕜 𝕜'] (x : 𝕜) : ∥algebra_map 𝕜' x∥ = ∥x∥ :=
id          └────────────┘  └┘           └─────────┘ └┘   
src         └────────────┘                 └─────────┘        
typ         └────────────┘  └┘           └─────────┘ └┘   
doc         └────────────┘
731  normed_algebra.norm_algebra_map_eq _ _
id   └────────────────────────────────┘
src  └────────────────────────────────┘
typ  └────────────────────────────────┘
732  
733  end normed_algebra
734  
735  section restrict_scalars
736  set_option class.instance_max_depth 40
doc             └──────────────────────┘
737  
738  variables (𝕜 : Type*) (𝕜' : Type*) [normed_field 𝕜] [normed_field 𝕜'] [normed_algebra 𝕜 𝕜']
id                                       └──────────┘     └──────────┘      └────────────┘
src                                      └──────────┘     └──────────┘      └────────────┘
typ                                      └──────────┘     └──────────┘      └────────────┘
doc                                      └──────────┘     └──────────┘      └────────────┘
739  {E : Type*} [normed_group E] [normed_space 𝕜' E]
id                └──────────┘     └──────────┘
src               └──────────┘     └──────────┘
typ               └──────────┘     └──────────┘
doc               └──────────┘     └──────────┘
740  
741  /-- `𝕜`-normed space structure induced by a `𝕜'`-normed space structure when `𝕜'` is a
742  normed algebra over `𝕜`. Not registered as an instance as `𝕜'` can not be inferred. -/
743  def normed_space.restrict_scalars : normed_space 𝕜 E :=
id                                       └──────────┘  
src                                      └──────────┘
typ                                      └──────────┘  
doc                                      └──────────┘
744  { norm_smul := λc x, begin
id                    
typ                   
st                        └─────
745      change ∥(algebra_map 𝕜' c) • x∥ = ∥c∥ * ∥x∥,
id               └─────────┘ └┘             
src      └─────┘ └─────────┘   └┘    
typ      └─────┘ └─────────┘└┘ └┘    
doc      └─────┘                └┘        
txt      └─────┘                └┘        
par      └─────┘                └┘        
pid                            └┘        
st   ──────────────────────────────────────────────┘└─
746      simp [norm_smul]
id             └───────┘
src      └────┘└───────┘└─
typ      └────┘└───────┘└─
doc      └────┘         └─
txt      └────┘         └─
par      └────┘         └─
pid                   
st   ─────────────────────
747    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
748    ..module.restrict_scalars 𝕜 𝕜' E }
id       └─────────────────────┘  └┘ 
src      └─────────────────────┘
typ      └─────────────────────┘  └┘ 
doc      └─────────────────────┘
749  
750  end restrict_scalars
751  
752  section summable
753  open_locale classical
754  open finset filter
755  variables [normed_group α] [complete_space α]
id             └──────────┘     └────────────┘
src             └──────────┘     └────────────┘
typ            └──────────┘     └────────────┘
doc             └──────────┘     └────────────┘
756  
757  lemma summable_iff_vanishing_norm {f : ι → α} :
id                                             
typ                                            
758    summable f ↔ ∀ε > 0, ∃s:finset ι, ∀t, disjoint t s → ∥ t.sum f ∥ < ε :=
id     └──────┘            └────┘     └──────┘      └──┘    
src    └──────┘              └────┘       └──────┘         └──┘    
typ    └──────┘            └────┘     └──────┘      └──┘    
doc    └──────┘                └────┘        └──────┘
759  begin
st   └─────
760    simp only [summable_iff_vanishing, metric.mem_nhds_iff, exists_imp_distrib],
id                └────────────────────┘  └─────────────────┘  └────────────────┘
src    └─────────┘└────────────────────┘└┘└─────────────────┘└┘└────────────────┘
typ    └─────────┘└────────────────────┘└┘└─────────────────┘└┘└────────────────┘
doc    └─────────┘                      └┘                   └┘                  
txt    └─────────┘                      └┘                   └┘                  
par    └─────────┘                      └┘                   └┘                  
pid        └──┘└┘                      └┘                   └┘                  
st   ────────────────────────────────────────────────────────────────────────────┘└─
761    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
762    { assume h ε hε, refine h {x | ∥x∥ < ε} ε hε _, rw [ball_0_eq ε] },
id                                         └┘        └───────┘ 
src      └───────────┘  └─────┘ └──┘  └┘   └┘  └──┘└───────┘ └┘
typ      └───────────┘  └─────┘└──┘  └┘└┘└┘  └──┘└───────┘└┘
doc      └───────────┘  └─────┘  └──┘     └┘   └┘  └──┘          └┘
txt      └───────────┘  └─────┘  └──┘     └┘   └┘  └──┘          └┘
par      └───────────┘  └─────┘  └──┘     └┘   └┘  └──┘          └┘
pid      └───────────┘          └──┘     └┘   └┘    └┘          
st   ───┘└───────────┘└─────────────────────────────┘└───────────────┘└┘
763    { assume h s ε hε hs,
src      └────────────────┘
typ      └────────────────┘
doc      └────────────────┘
txt      └────────────────┘
par      └────────────────┘
pid      └────────────────┘
st   ─────────────────────┘└─
764      rcases h ε hε with ⟨t, ht⟩,
id                └┘
src      └─────┘    └───────────┘
typ      └─────┘└┘└───────────┘
doc      └─────┘    └───────────┘
txt      └─────┘    └───────────┘
par      └─────┘    └───────────┘
pid                └───────────┘
st   ─────────────────────────────┘└─
765      refine ⟨t, assume u hu, hs _⟩,
id                              └┘
src      └─────┘  └┘      └─────┘  └─┘
typ      └─────┘ └┘      └─────┘└┘└─┘
doc      └─────┘  └┘      └─────┘  └─┘
txt      └─────┘  └┘      └─────┘  └─┘
par      └─────┘  └┘      └─────┘  └─┘
pid              └┘      └─────┘  └─┘
st   ────────────────────────────────┘└─
766      rw [ball_0_eq],
id           └───────┘
src      └──┘└───────┘
typ      └──┘└───────┘
doc      └──┘         
txt      └──┘         
par      └──┘         
pid        └┘         
st   ────────────────┘└──
767      exact ht u hu }
id             └┘  └┘
src      └────┘     
typ      └────┘└┘└┘
doc      └────┘     
txt      └────┘     
par      └────┘     
pid                
st   ─────────────────┘└─
768  end
st   ──┘
769  
770  lemma summable_of_norm_bounded {f : ι → α} (g : ι → ℝ) (hf : summable g) (h : ∀i, ∥f i∥ ≤ g i) :
id                                                            └──────┘               
src                                                              └──────┘                 
typ                                                           └──────┘               
doc                                                               └──────┘
771    summable f :=
id     └──────┘ 
src    └──────┘
typ    └──────┘ 
doc    └──────┘
772  summable_iff_vanishing_norm.2 $ assume ε hε,
id   └─────────────────────────┘            └┘
src  └─────────────────────────┘
typ  └─────────────────────────┘            └┘
773    let ⟨s, hs⟩ := summable_iff_vanishing_norm.1 hf ε hε in
id     └─┘    └┘     └─────────────────────────┘  └┘  └┘
src                   └─────────────────────────┘
typ    └─┘    └┘     └─────────────────────────┘  └┘  └┘
774    ⟨s, assume t ht,
id                 └┘
typ                └┘
775      have ∥t.sum g∥ < ε := hs t ht,
id            └──┘           └┘
src            └──┘   
typ           └──┘           └┘
776      have nn : 0 ≤ t.sum g := finset.sum_nonneg (assume a _, le_trans (norm_nonneg _) (h a)),
id                    └──┘     └───────────────┘            └──────┘  └─────────┘      
src                    └──┘      └───────────────┘              └──────┘  └─────────┘
typ                   └──┘     └───────────────┘            └──────┘  └─────────┘      
777      lt_of_le_of_lt (norm_sum_le_of_le t (λ i _, h i)) $
id       └────────────┘  └───────────────┘         
src      └────────────┘  └───────────────┘
typ      └────────────┘  └───────────────┘         
778        by rwa [real.norm_eq_abs, abs_of_nonneg nn] at this⟩
id                 └──────────────┘  └───────────┘ └┘
src           └───┘└──────────────┘└┘└───────────┘  └───────┘
typ           └───┘└──────────────┘└┘└───────────┘└┘└───────┘
doc           └───┘                └┘               └───────┘
txt           └───┘                └┘               └───────┘
par           └───┘                └┘               └───────┘
pid              └┘                └┘               └──────┘
st           └────────────────────┘└────────────────┘└──────┘
779  
780  lemma summable_of_summable_norm {f : ι → α} (hf : summable (λa, ∥f a∥)) : summable f :=
id                                                   └──────┘           └──────┘ 
src                                                    └──────┘              └──────┘
typ                                                  └──────┘           └──────┘ 
doc                                                    └──────┘                └──────┘
781  summable_of_norm_bounded _ hf (assume i, le_refl _)
id   └──────────────────────┘   └┘           └─────┘
src  └──────────────────────┘                 └─────┘
typ  └──────────────────────┘   └┘           └─────┘
782  
783  lemma norm_tsum_le_tsum_norm {f : ι → α} (hf : summable (λi, ∥f i∥)) : ∥(∑i, f i)∥ ≤ (∑ i, ∥f i∥) :=
id                                                └──────┘                     
src                                                 └──────┘                              
typ                                               └──────┘                     
doc                                                 └──────┘                               
784  have h₁ : tendsto (λs:finset ι, ∥s.sum f∥) at_top (𝓝 ∥(∑ i, f i)∥) :=
id             └─────┘     └────┘   └──┘   └────┘        
src            └─────┘     └────┘     └──┘    └────┘           
typ            └─────┘     └────┘   └──┘   └────┘        
doc            └─────┘     └────┘               └────┘       
785    (continuous_norm.tendsto _).comp (has_sum_tsum $ summable_of_summable_norm hf),
id      └─────────────┘└──────┘   └──┘   └──────────┘   └───────────────────────┘ └┘
src     └─────────────┘└──────┘   └──┘   └──────────┘   └───────────────────────┘
typ     └─────────────┘└──────┘   └──┘   └──────────┘   └───────────────────────┘ └┘
786  have h₂ : tendsto (λs:finset ι, s.sum (λi, ∥f i∥)) at_top (𝓝 (∑ i, ∥f i∥)) :=
id             └─────┘     └────┘   └──┘         └────┘       
src            └─────┘     └────┘     └──┘            └────┘          
typ            └─────┘     └────┘   └──┘         └────┘       
doc            └─────┘     └────┘                       └────┘      
787    has_sum_tsum hf,
id     └──────────┘ └┘
src    └──────────┘
typ    └──────────┘ └┘
788  le_of_tendsto_of_tendsto at_top_ne_bot h₁ h₂ $ univ_mem_sets' $ assume s, norm_sum_le _ _
id   └──────────────────────┘ └───────────┘ └┘ └┘   └────────────┘            └─────────┘
src  └──────────────────────┘ └───────────┘         └────────────┘             └─────────┘
typ  └──────────────────────┘ └───────────┘ └┘ └┘   └────────────┘            └─────────┘
789  
790  end summable